awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)
hμ : g = HAdd.hAdd (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) n
h :
  ∀ (x : M),
    Eq (α := M) ((f ∘ₗ (algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) μ : (a : M) → M) x : M)
      ((μ • f : (a : M) → M) x : M)
⊢ f ∘ₗ (algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) μ = μ • f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)
hμ : g = HAdd.hAdd (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) n
x : M
⊢ Eq (α := M) ((f ∘ₗ (algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) μ : (a : M) → M) x : M)
    ((μ • f : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)
hμ : g = HAdd.hAdd (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) n
⊢ f ∘ₗ (algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) μ = μ • f

Tactic:
have : f ∘ₗ algebraMap R _ μ = μ • f := by ext; simp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)
hμ : g = HAdd.hAdd (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) μ = μ • f
rw :
  (trace R M : (a : M →ₗ[R] M) → R)
      (f ∘ₗ HAdd.hAdd (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) n) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₁ :
  (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ (algebraMap R (End R M) : (a : R) → End R M) μ + f ∘ₗ n) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₂ :
  HAdd.hAdd (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ (algebraMap R (End R M) : (a : R) → End R M) μ) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₃ :
  HAdd.hAdd (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ (algebraMap R (End R M) : (a : R) → End R M) μ) : R) (0 : R) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₄ :
  (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ (algebraMap R (End R M) : (a : R) → End R M) μ) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₅ : (trace R M : (a : M →ₗ[R] M) → R) (μ • f) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₆ :
  HSMul.hSMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₇ rw₈ :
  HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R) =
    HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]

Premises used: map_add, LinearMap.comp_add, smul_eq_mul, add_zero, map_smul
-- Module: Mathlib.LinearAlgebra.Trace
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
A : Type u_6
inst_5 : CommRing A
inst_6 : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
change :
  Eq.{u_6 + 1} (α := A) ((trace A (A ⊗[R] M) : (a : A ⊗[R] M →ₗ[A] A ⊗[R] M) → A) (baseChange A f) : A)
    (((↑(algebraMap R A) : R →+ A) : (a : R) → A) ((trace R M : (a : M →ₗ[R] M) → R) f : R) : A)
⊢ Eq.{u_6 + 1} (α := A) ((trace A (A ⊗[R] M) : (a : A ⊗[R] M →ₗ[A] A ⊗[R] M) → A) (baseChange A f) : A)
    ((algebraMap R A : (a : R) → A) ((trace R M : (a : M →ₗ[R] M) → R) f : R) : A)

Tactic:
change _ = (algebraMap R A : R →+ A) _

Premises used: Algebra.algebraMap, AddMonoidHomClass.toAddMonoidHom, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Trace
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
A : Type u_6
inst_5 : CommRing A
inst_6 : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ Eq.{u_6 + 1} (α := A) ((trace A (A ⊗[R] M) : (a : A ⊗[R] M →ₗ[A] A ⊗[R] M) → A) (baseChange A f) : A)
    (((↑(algebraMap R A) : R →+ A) : (a : R) → A) ((trace R M : (a : M →ₗ[R] M) → R) f : R) : A)

Tactic:
simp [b', trace_eq_matrix_trace R b, trace_eq_matrix_trace A b', AddMonoidHom.map_trace]

Premises used: AddMonoidHom.map_trace, LinearMap.trace_eq_matrix_trace
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
⊢ 0 < finrank R S

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
⊢ Module.Finite R S

Tactic:
have : Module.Finite R S := finite_of_finrank_pos (by grind)
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this : Module.Finite R S
⊢ Free.{u_1, u_2} R (End R S)

Tactic:
have : Free R (Module.End R S) := .of_equiv (dualTensorHomEquiv R S S)
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h₁ :
  Eq (α := R)
    ((LinearMap.trace R S ∘ₗ
            (↑f :
                [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
                  [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
              Algebra.linearMap R S :
          (a : R) → R)
        1 :
      R)
    ((LinearMap.id : (a : R) → R) 1 : R)
⊢ LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
⊢ Eq (α := R)
    ((LinearMap.trace R S ∘ₗ
            (↑f :
                [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
                  [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
              Algebra.linearMap R S :
          (a : R) → R)
        1 :
      R)
    ((LinearMap.id : (a : R) → R) 1 : R)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
⊢ LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id

Tactic:
have h1 : LinearMap.trace R S ∘ₗ f ∘ₗ Algebra.linearMap R S = LinearMap.id := by ext; simp [h]
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 :
  LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id
b : Basis.{0, u_1, u_2} (Unit × Unit) R (End R S) :=
  Basis.map
    ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h) :
      Basis (Unit × Unit) R (TensorProduct R (Dual R S) S))
    (dualTensorHomEquiv R S S : TensorProduct R (Dual R S) S ≃ₗ[R] S →ₗ[R] S)
i : Unit × Unit
j : Unit
⊢ Eq (α := S)
    ((((((↑f :
                      [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
                        [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
                    Algebra.linearMap R S) ∘ₗ
                  LinearMap.trace R S :
                (a : End R S) → S →ₗ[R] S)
              ((b : (a : Unit × Unit) → End R S) i : End R S) :
            S →ₗ[R] S) :
          (a : S) → S)
        ((basisUnique Unit h : (a : Unit) → S) j : S) :
      S)
    ((((LinearMap.id : (a : End R S) → S →ₗ[R] S) ((b : (a : Unit × Unit) → End R S) i : End R S) : S →ₗ[R] S) :
          (a : S) → S)
        ((basisUnique Unit h : (a : Unit) → S) j : S) :
      S)

Tactic:
simp [f, b, Basis.tensorProduct]

Premises used: Module.Basis.tensorProduct
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 :
  LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id
b : Basis.{0, u_1, u_2} (Unit × Unit) R (End R S) :=
  Basis.map
    ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h) :
      Basis (Unit × Unit) R (TensorProduct R (Dual R S) S))
    (dualTensorHomEquiv R S S : TensorProduct R (Dual R S) S ≃ₗ[R] S →ₗ[R] S)
⊢ Eq (α := (S →ₗ[R] S) →ₗ[R] S →ₗ[R] S)
    (((↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S) ∘ₗ
      LinearMap.trace R S)
    LinearMap.id

Tactic:
have h2 : (f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id :=
    b.ext fun i ↦
      (basisUnique Unit h).ext fun j ↦ (by simp [f, b, Basis.tensorProduct])
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 :
  LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id
b : Basis.{0, u_1, u_2} (Unit × Unit) R (End R S) :=
  Basis.map
    ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h) :
      Basis (Unit × Unit) R (TensorProduct R (Dual R S) S))
    (dualTensorHomEquiv R S S : TensorProduct R (Dual R S) S ≃ₗ[R] S →ₗ[R] S)
h2 :
  Eq (α := (S →ₗ[R] S) →ₗ[R] S →ₗ[R] S)
    (((↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S) ∘ₗ
      LinearMap.trace R S)
    LinearMap.id
eq : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R) R (End R S) :=
  LinearEquiv.ofLinear
    ((↑f :
        [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
          [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
      Algebra.linearMap R S)
    (LinearMap.trace R S) h2 h1
⊢ Function.Bijective (α := S) (β := S →ₗ[R] S) (⇑f : (a : S) → S →ₗ[R] S)

Tactic:
have hf : Function.Bijective f := ⟨Algebra.lmul_injective, .of_comp eq.surjective⟩
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 :
  LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id
b : Basis.{0, u_1, u_2} (Unit × Unit) R (End R S) :=
  Basis.map
    ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h) :
      Basis (Unit × Unit) R (TensorProduct R (Dual R S) S))
    (dualTensorHomEquiv R S S : TensorProduct R (Dual R S) S ≃ₗ[R] S →ₗ[R] S)
h2 :
  Eq (α := (S →ₗ[R] S) →ₗ[R] S →ₗ[R] S)
    (((↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S) ∘ₗ
      LinearMap.trace R S)
    LinearMap.id
eq : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R) R (End R S) :=
  LinearEquiv.ofLinear
    ((↑f :
        [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
          [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
      Algebra.linearMap R S)
    (LinearMap.trace R S) h2 h1
hf : Function.Bijective (α := S) (β := S →ₗ[R] S) (⇑f : (a : S) → S →ₗ[R] S)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
(Function.Bijective.of_comp_iff' hf _).mp eq.bijective

Premises used: LinearEquiv.bijective, Function.Bijective.of_comp_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : Free R S
h : finrank R S = 1
this_1 : Module.Finite R S
this : Free.{u_1, u_2} R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 :
  LinearMap.trace R S ∘ₗ
      (↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S =
    LinearMap.id
b : Basis.{0, u_1, u_2} (Unit × Unit) R (End R S) :=
  Basis.map
    ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h) :
      Basis (Unit × Unit) R (TensorProduct R (Dual R S) S))
    (dualTensorHomEquiv R S S : TensorProduct R (Dual R S) S ≃ₗ[R] S →ₗ[R] S)
h2 :
  Eq (α := (S →ₗ[R] S) →ₗ[R] S →ₗ[R] S)
    (((↑f :
          [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
            [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
        Algebra.linearMap R S) ∘ₗ
      LinearMap.trace R S)
    LinearMap.id
eq : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R) R (End R S) :=
  LinearEquiv.ofLinear
    ((↑f :
        [inst_5 : FunLike (S →ₐ[R] S →ₗ[R] S) S (S →ₗ[R] S)] →
          [SemilinearMapClass (S →ₐ[R] S →ₗ[R] S) (RingHom.id R) S (S →ₗ[R] S)] → S →ₗ[R] S →ₗ[R] S) ∘ₗ
      Algebra.linearMap R S)
    (LinearMap.trace R S) h2 h1
hf : Function.Bijective (α := S) (β := S →ₗ[R] S) (⇑f : (a : S) → S →ₗ[R] S)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
exact (Function.Bijective.of_comp_iff' hf _).mp eq.bijective

Premises used: LinearEquiv.bijective, Function.Bijective.of_comp_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v x y : V
⊢ x + y + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) (x + y) : R) v =
    x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v +
      (y + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) y : R) v)

Tactic:
simp [add_add_add_comm, add_smul]

Premises used: add_smul, add_add_add_comm
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v : V
r : R
x : V
⊢ r • x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) (r • x) : R) v =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v)

Tactic:
simp [smul_eq_mul, smul_add, mul_smul]

Premises used: smul_eq_mul, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v x : V
⊢ (transvection f v : (a : V) → V) x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v w x : V
hw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) w : R) (0 : R)
⊢ Eq (α := V) ((transvection f v : (a : V) → V) ((transvection f w : (a : V) → V) x : V) : V)
    ((transvection f (v + w) : (a : V) → V) x : V)

Tactic:
simp [transvection, map_add, hw, add_assoc]

Premises used: LinearMap.transvection, add_assoc, map_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v w : V
hw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) w : R) (0 : R)
h :
  ∀ (x : V),
    Eq (α := V) ((transvection f v ∘ₗ transvection f w : (a : V) → V) x : V)
      ((transvection f (v + w) : (a : V) → V) x : V)
⊢ transvection f v ∘ₗ transvection f w = transvection f (v + w)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v w : V
hw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) w : R) (0 : R)
x : V
⊢ Eq (α := V) ((transvection f v ∘ₗ transvection f w : (a : V) → V) x : V)
    ((transvection f (v + w) : (a : V) → V) x : V)

Tactic:
simp [comp_of_left_eq_apply hw]

Premises used: LinearMap.transvection.comp_of_left_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f g : Dual R V
v x : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Eq (α := V) ((transvection f v : (a : V) → V) ((transvection g v : (a : V) → V) x : V) : V)
    ((transvection (f + g) v : (a : V) → V) x : V)

Tactic:
simp [transvection, map_add, hf, add_smul, add_assoc]

Premises used: LinearMap.transvection, add_assoc, map_add, add_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f g : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h :
  ∀ (x : V),
    Eq (α := V) ((transvection f v ∘ₗ transvection g v : (a : V) → V) x : V)
      ((transvection (f + g) v : (a : V) → V) x : V)
⊢ transvection f v ∘ₗ transvection g v = transvection (f + g) v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f g : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ Eq (α := V) ((transvection f v ∘ₗ transvection g v : (a : V) → V) x : V)
    ((transvection (f + g) v : (a : V) → V) x : V)

Tactic:
simp [comp_of_right_eq_apply hf]

Premises used: LinearMap.transvection.comp_of_right_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
v : V
h : ∀ (x : V), Eq (α := V) ((transvection 0 v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
⊢ Eq (α := V →ₗ[R] V) (transvection 0 v) id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
v x : V
⊢ Eq (α := V) ((transvection 0 v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)

Tactic:
simp [transvection]

Premises used: LinearMap.transvection
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
h : ∀ (x : V), Eq (α := V) ((transvection f 0 : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
⊢ transvection f 0 = id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
x : V
⊢ Eq (α := V) ((transvection f 0 : (a : V) → V) x : V) ((id : (a : V) → V) x : V)

Tactic:
simp [transvection]

Premises used: LinearMap.transvection
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v : V
r s : R
h :
  ∀ (x : V),
    Eq (α := V) ((transvection f (r • v) ∘ₗ transvection f (s • v) : (a : V) → V) x : V)
      ((transvection f ((r + s + HMul.hMul (β := R) s ((f : (a : V) → R) v : R) * r) • v) : (a : V) → V) x : V)
⊢ transvection f (r • v) ∘ₗ transvection f (s • v) =
    transvection f ((r + s + HMul.hMul (β := R) s ((f : (a : V) → R) v : R) * r) • v)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v : V
r s : R
x : V
h :
  x +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) (r • v) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R)
          (s • (v + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) v : R) (r • v)))) =
    x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R)
        ((r + (s + HMul.hMul (β := R) s ((f : (a : V) → R) v : R) * r)) • v)
⊢ Eq (α := V) ((transvection f (r • v) ∘ₗ transvection f (s • v) : (a : V) → V) x : V)
    ((transvection f ((r + s + HMul.hMul (β := R) s ((f : (a : V) → R) v : R) * r) • v) : (a : V) → V) x : V)

Tactic:
simp only [LinearMap.comp_apply, apply, map_add, map_smul, add_assoc]

Premises used: add_assoc, LinearMap.comp_apply, map_add, LinearMap.transvection.apply, map_smul