awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
rw :
  Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
    (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
rw₂ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₃ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑(e.symm ≪≫ₗ f) : M' →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)
have rw₄ : Eq.{u_1 + 1} (α := R)
  ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑f : M →ₗ[R] M) ∘ₗ (↑e.symm : M' →ₗ[R] M)) : R)
  ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
Tactic: rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
rw :
  Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
    (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
rw₂ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₃ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑(e.symm ≪≫ₗ f) : M' →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₄ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑f : M →ₗ[R] M) ∘ₗ (↑e.symm : M' →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)
have rw₅ : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
  ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
Tactic: rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) (↑f : M →ₗ[R] M')))
have h : HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
    ((toMatrix v' v : (a : M' →ₗ[R] M) → Matrix ι ι R) (↑f.symm : M' →ₗ[R] M) : Matrix ι ι R)
    ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) (↑f : M →ₗ[R] M') : Matrix ι ι R) =
  1
Tactic: apply isUnit_det_of_left_inverse
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h :
  HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
      ((toMatrix v' v : (a : M' →ₗ[R] M) → Matrix ι ι R) (↑f.symm : M' →ₗ[R] M) : Matrix ι ι R)
      ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) (↑f : M →ₗ[R] M') : Matrix ι ι R) =
    1
⊢ IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) (↑f : M →ₗ[R] M')))
have B : Matrix ι ι R
Tactic: apply isUnit_det_of_left_inverse
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M
⊢ Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    ((((toLin v v : (a : Matrix ι ι R) → M →ₗ[R] M)
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)) :
            M →ₗ[R] M) :
          (a : M) → M)
        x :
      M)
have rw : Eq.{u_2 + 1} (α := M)
  ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          M' →ₗ[R] M) :
        (a : M') → M)
      ((f : (a : M) → M') x : M') :
    M)
  (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ
          (toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
        (a : M) → M)
      x :
    M)
Tactic: rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M
rw :
  Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ
            (toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
          (a : M) → M)
        x :
      M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    ((((toLin v v : (a : Matrix ι ι R) → M →ₗ[R] M)
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)) :
            M →ₗ[R] M) :
          (a : M) → M)
        x :
      M)
have rw₁ : Eq.{u_2 + 1} (α := M)
  ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          M' →ₗ[R] M) :
        (a : M') → M)
      ((f : (a : M) → M') x : M') :
    M)
  (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ f :
        (a : M) → M)
      x :
    M)
Tactic: rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M
rw :
  Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ
            (toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
          (a : M) → M)
        x :
      M)
rw₁ :
  Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ f :
          (a : M) → M)
        x :
      M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    ((((toLin v v : (a : Matrix ι ι R) → M →ₗ[R] M)
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)) :
            M →ₗ[R] M) :
          (a : M) → M)
        x :
      M)
have rw₂ : Eq.{u_2 + 1} (α := M)
  ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          M' →ₗ[R] M) :
        (a : M') → M)
      ((f : (a : M) → M') x : M') :
    M)
  ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          M' →ₗ[R] M) :
        (a : M') → M)
      ((f : (a : M) → M') x : M') :
    M)
Tactic: rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M'
⊢ Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((((toLin v' v' : (a : Matrix ι ι R) → M' →ₗ[R] M')
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)) :
            M' →ₗ[R] M') :
          (a : M') → M')
        x :
      M')
have rw : Eq.{u_3 + 1} (α := M')
  ((f : (a : M) → M')
      ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
              M' →ₗ[R] M) :
            (a : M') → M)
          x :
        M) :
    M')
  (((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) ∘ₗ
          (toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
        (a : M') → M')
      x :
    M')
Tactic: rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M'
rw :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    (((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) ∘ₗ
            (toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          (a : M') → M')
        x :
      M')
⊢ Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((((toLin v' v' : (a : Matrix ι ι R) → M' →ₗ[R] M')
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)) :
            M' →ₗ[R] M') :
          (a : M') → M')
        x :
      M')
have rw₁ : Eq.{u_3 + 1} (α := M')
  ((f : (a : M) → M')
      ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
              M' →ₗ[R] M) :
            (a : M') → M)
          x :
        M) :
    M')
  ((((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
          M →ₗ[R] M') :
        (a : M) → M')
      ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
              M' →ₗ[R] M) :
            (a : M') → M)
          x :
        M) :
    M')
Tactic: rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M'
rw :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    (((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) ∘ₗ
            (toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          (a : M') → M')
        x :
      M')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
            M →ₗ[R] M') :
          (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
⊢ Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((((toLin v' v' : (a : Matrix ι ι R) → M' →ₗ[R] M')
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)) :
            M' →ₗ[R] M') :
          (a : M') → M')
        x :
      M')
have rw₂ : Eq.{u_3 + 1} (α := M')
  ((f : (a : M) → M')
      ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
              M' →ₗ[R] M) :
            (a : M') → M)
          x :
        M) :
    M')
  ((f : (a : M) → M')
      ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
              M' →ₗ[R] M) :
            (a : M') → M)
          x :
        M) :
    M')
Tactic: rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
⊢ (↑(ofIsUnitDet h) : M →ₗ[R] M') = f
have h₁ : ∀ (x : M), Eq.{u_3 + 1} (α := M') (((↑(ofIsUnitDet h) : M →ₗ[R] M') : (a : M) → M') x : M') ((f : (a : M) → M') x : M')
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
⊢ M ≃ₗ[R] M
have pos : (hR : Nontrivial R) → M ≃ₗ[R] M
Tactic: by_cases hR : Nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
pos : (hR : Nontrivial R) → M ≃ₗ[R] M
⊢ M ≃ₗ[R] M
have neg : (hR : ¬Nontrivial R) → M ≃ₗ[R] M
Tactic: by_cases hR : Nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
⊢ M ≃ₗ[R] M
have pos : (ι : Type u_2) → (b : Basis ι R M) → M ≃ₗ[R] M
Tactic: let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
⊢ M ≃ₗ[R] M
have this : Finite ι
Tactic: have : Finite ι := Module.Finite.finite_basis b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this : Finite ι
⊢ M ≃ₗ[R] M
have pos : (this : Fintype ι) → M ≃ₗ[R] M
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this_1 : Finite ι
this : Fintype ι
⊢ M ≃ₗ[R] M
have pos : (this : DecidableEq ι) → M ≃ₗ[R] M
Tactic: have : DecidableEq ι := Classical.typeDecidableEq ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (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
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
x : M
⊢ Eq (α := M) ((equivOfIsUnitDet h : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (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
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
⊢ (↑(equivOfIsUnitDet h) : M →ₗ[R] M) = f
have h₁ : ∀ (x : M), Eq (α := M) (((↑(equivOfIsUnitDet h) : M →ₗ[R] M) : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M_1
𝕜 : Type u_5
inst_7 : Field 𝕜
M : Type u_6
inst_8 : AddCommGroup M
inst_9 : Module 𝕜 M
inst_10 : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : Ne.{u_5 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ IsUnit.{u_5} (M := 𝕜)
    (det (n := Fin (finrank 𝕜 M))
      (((toMatrix (finBasis 𝕜 M) (finBasis 𝕜 M) :
            LinearEquiv.{u_5, u_5, u_6, u_5} (RingHom.id 𝕜) (M →ₗ[𝕜] M)
              (Matrix (Fin (finrank 𝕜 M)) (Fin (finrank 𝕜 M)) 𝕜)) :
          (a : M →ₗ[𝕜] M) → Matrix (Fin (finrank 𝕜 M)) (Fin (finrank 𝕜 M)) 𝕜)
        f))
have rw : IsUnit.{u_5} (M := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜)
Tactic: rw [LinearMap.det_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
have h₁ : f = f' ∘ₗ (↑e : M →ₗ[R] M)
Tactic: convert! this using 2