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
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
have 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)
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
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
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have this : f ∘ₗ (algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) μ = μ • f
Tactic: have : f ∘ₗ algebraMap R _ μ = μ • f := by ext; simp
-- 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 : 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
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have rw₅ : (trace R M : (a : M →ₗ[R] M) → R) (μ • f) = 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]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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 : 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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]
-- 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
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 : (a : R) → A) ((trace R M : (a : M →ₗ[R] M) → R) f : R) : A)
have 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)
Tactic: change _ = (algebraMap R A : R →+ A) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have this : Module.Finite R S
Tactic: have : Module.Finite R S := finite_of_finrank_pos (by grind)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have this₁ : Free.{u_1, u_2} R (End R S)
Tactic: have : Free R (Module.End R S) := .of_equiv (dualTensorHomEquiv R S S)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have 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
Tactic: have h1 : LinearMap.trace R S ∘ₗ f ∘ₗ Algebra.linearMap R S = LinearMap.id := by ext; simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have 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
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])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have hf : 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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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)
⊢ transvection f v ∘ₗ transvection f w = transvection f (v + w)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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)
⊢ transvection f v ∘ₗ transvection g v = transvection (f + g) v
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
v : V
⊢ Eq (α := V →ₗ[R] V) (transvection 0 v) id
have h : ∀ (x : V), Eq (α := V) ((transvection 0 v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ transvection f 0 = id
have h : ∀ (x : V), Eq (α := V) ((transvection f 0 : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ transvection f (r • v) ∘ₗ transvection f (s • v) =
    transvection f ((r + s + HMul.hMul (β := R) s ((f : (a : V) → R) v : R) * r) • v)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have 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)
Tactic: simp only [LinearMap.comp_apply, apply, map_add, map_smul, add_assoc]