awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
obtain :
  ∀ (v : Fin (finrank R M) → R) (hv_ne_zero : v ≠ 0)
    (hv_zero :
      Eq (α := Fin (finrank R M) → R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0),
    ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
⊢ ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0

Tactic:
obtain ⟨v, hv_ne_zero, hv_zero⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr (det_toMatrix b f ▸ hf)

Premises used: Iff.mpr, Matrix.exists_mulVec_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero :
  Eq (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
⊢ ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0

Tactic:
⟨b.equivFun.symm v, ?_, b.equivFun.symm.map_ne_zero_iff.mpr hv_ne_zero⟩

Premises used: Iff.mpr, LinearEquiv.symm, And.intro, Exists.intro, LinearEquiv.map_ne_zero_iff, DFunLike.coe, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero :
  Eq (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
refine : Eq (α := M) ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) (0 : M)
⊢ ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0

Tactic:
refine ⟨b.equivFun.symm v, ?_, b.equivFun.symm.map_ne_zero_iff.mpr hv_ne_zero⟩
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero :
  Eq (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
rw :
  Eq.{u_1 + 1} (α := Fin (finrank R M) → R)
    ((b.equivFun : (a : M) → Fin (finrank R M) → R)
        ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) :
      Fin (finrank R M) → R)
    ((b.equivFun : (a : M) → Fin (finrank R M) → R) 0 : Fin (finrank R M) → R)
⊢ Eq (α := M) ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) (0 : M)

Tactic:
rw [← b.equivFun.injective.eq_iff]

Premises used: Function.Injective.eq_iff, LinearEquiv.injective, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero :
  Eq (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
⊢ Eq.{u_1 + 1} (α := Fin (finrank R M) → R)
    ((b.equivFun : (a : M) → Fin (finrank R M) → R)
        ((f : (a : M) → M) ((b.equivFun.symm : (a : Fin (finrank R M) → R) → M) v : M) : M) :
      Fin (finrank R M) → R)
    ((b.equivFun : (a : M) → Fin (finrank R M) → R) 0 : Fin (finrank R M) → R)

Tactic:
simp_all [funext_iff, Matrix.mulVec, dotProduct, toMatrix_apply, mul_comm]

Premises used: dotProduct, funext_iff, mul_comm, Matrix.mulVec, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
mp : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R) → f.ker ≠ ⊥
mpr : f.ker ≠ ⊥ → Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R) ↔ f.ker ≠ ⊥

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ f.ker ≠ ⊥

Tactic:
bot_lt_iff_ne_bot.mp (bot_lt_ker_of_det_eq_zero h)

Premises used: LinearMap.bot_lt_ker_of_det_eq_zero, bot_lt_iff_ne_bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ f.ker ≠ ⊥

Tactic:
exact bot_lt_iff_ne_bot.mp (bot_lt_ker_of_det_eq_zero h)

Premises used: LinearMap.bot_lt_ker_of_det_eq_zero, bot_lt_iff_ne_bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
mpr : ∀ v ∈ f.ker, ∀ (hv_ne_zero : v ≠ 0), Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)

Tactic:
obtain ⟨v, ⟨_, hv_ne_zero⟩⟩ := (ker f).ne_bot_iff.mp h

Premises used: LinearMap.ker, Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left : v ∈ f.ker
hv_ne_zero : v ≠ 0
mpr :
  ∃ (v : Fin (finrank R M) → R),
    v ≠ 0 ∧
      Eq (α := Fin (finrank R M) → R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)

Tactic:
rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]

Premises used: Matrix.exists_mulVec_eq_zero_iff, LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left : v ∈ f.ker
hv_ne_zero : v ≠ 0
⊢ Ne.{u_1 + 1} (α := Fin (finrank R M) → R)
    (fun (i : Fin (finrank R M)) ↦
      (((b.repr : (a : M) → Fin (finrank R M) →₀ R) v : Fin (finrank R M) →₀ R) : (a : Fin (finrank R M)) → R) i)
    0

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left : v ∈ f.ker
hv_ne_zero : v ≠ 0
⊢ Eq.{max 1 (u_1 + 1)} (α := Fin (finrank R M) → R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ
      fun (i : Fin (finrank R M)) ↦
      (((b.repr : (a : M) → Fin (finrank R M) →₀ R) v : Fin (finrank R M) →₀ R) : (a : Fin (finrank R M)) → R) i)
    0

Tactic:
simpa [toMatrix_mulVec_repr]

Premises used: LinearMap.toMatrix_mulVec_repr
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Free R M
inst_5 : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left : v ∈ f.ker
hv_ne_zero : v ≠ 0
⊢ ∃ (v : Fin (finrank R M) → R),
    v ≠ 0 ∧
      Eq (α := Fin (finrank R M) → R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f *ᵥ v) 0

Tactic:
refine ⟨fun i => b.repr v i, by simpa, by simpa [toMatrix_mulVec_repr]⟩
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ Module.Finite 𝕜 M

Tactic:
simp [finite_of_det_ne_one (f := f), hf]

Premises used: LinearMap.finite_of_det_ne_one
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ Module.Finite 𝕜 M

Tactic:
have : Module.Finite 𝕜 M := by simp [finite_of_det_ne_one (f := f), hf]
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
this : Module.Finite 𝕜 M
rw : ⊥ < f.ker
⊢ f.range < ⊤

Tactic:
rw [lt_top_iff_ne_top, ne_eq, ← ker_eq_bot_iff_range_eq_top, ← ne_eq, ← bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot, lt_top_iff_ne_top, ne_eq, LinearMap.ker_eq_bot_iff_range_eq_top
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
this : Module.Finite 𝕜 M
⊢ ⊥ < f.ker

Tactic:
bot_lt_ker_of_det_eq_zero hf

Premises used: LinearMap.bot_lt_ker_of_det_eq_zero
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_7
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
this : Module.Finite 𝕜 M
⊢ ⊥ < f.ker

Tactic:
exact bot_lt_ker_of_det_eq_zero hf

Premises used: LinearMap.bot_lt_ker_of_det_eq_zero
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
f : R →ₗ[R] R
⊢ Eq (α := R) (((LinearMap.det.{u_1, u_1} (M := R) (A := R) : (R →ₗ[R] R) →* R) : (a : R →ₗ[R] R) → R) f : R)
    ((f : (a : R) → R) 1 : R)

Tactic:
simp [← det_toMatrix (Basis.singleton Unit R)]

Premises used: Unit, Module.Basis.singleton, LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
a : R
⊢ ((LinearMap.det.{u_1, u_1} (M := R) (A := R) : (R →ₗ[R] R) →* R) : (a : R →ₗ[R] R) → R) (mulLeft R a) = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
a : R
⊢ ((LinearMap.det.{u_1, u_1} (M := R) (A := R) : (R →ₗ[R] R) →* R) : (a : R →ₗ[R] R) → R) (mulRight R a) = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
simp_rw :
  Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := (i : ι) → M) (A := R) : (((i : ι) → M) →ₗ[R] (i : ι) → M) →* R) :
          (a : ((i : ι) → M) →ₗ[R] (i : ι) → M) → R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i :
          ((i : ι) → M) →ₗ[R] (i : ι) → M) :
      R)
    (∏ i : ι, (LinearMap.det : (a : M →ₗ[R] M) → R) (f i) : R)

Tactic:
simp_rw [← LinearMap.det_toMatrix B, ← LinearMap.det_toMatrix b]

Premises used: LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
a :
  ∀ (i₁ : Free.ChooseBasisIndex R M) (i₂ : ι) (j₁ : Free.ChooseBasisIndex R M) (j₂ : ι),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix B B :
            (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
              Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
          (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) (i₁, i₂) (j₁, j₂) :
        R)
      (blockDiagonal
          (fun (i : ι) ↦
            (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i))
          (i₁, i₂) (j₁, j₂) :
        R)
⊢ Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
a :
  Eq.{u_1 + 1} (α := R)
    ((toMatrix
            (Basis.reindex
              (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
              (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M))
                (Equiv.prodComm ι (Free.ChooseBasisIndex R M))))
            (Basis.reindex
              (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
              (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M))
                (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))) :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) (i₁, i₂) (j₁, j₂) :
      R)
    (blockDiagonal
        (fun (i : ι) ↦
          (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i))
        (i₁, i₂) (j₁, j₂) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) (i₁, i₂) (j₁, j₂) :
      R)
    (blockDiagonal
        (fun (i : ι) ↦
          (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i))
        (i₁, i₂) (j₁, j₂) :
      R)

Tactic:
unfold B
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
pos :
  ∀ (h : i₂ = j₂),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁ :
        R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁ :
        R)
neg :
  ∀ (h : ¬i₂ = j₂),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R) ((f i₂ : (a : M) → M) 0) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁ :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) (if i₂ = j₂ then (b : (a : Free.ChooseBasisIndex R M) → M) j₁ else 0 : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    (if i₂ = j₂ then
        (((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁
      else 0 :
      R)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
h : i₂ = j₂
pos pos₁ :
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f j₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f j₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
h : ¬i₂ = j₂
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R) ((f i₂ : (a : M) → M) 0) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    (0 : R)

Tactic:
simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, map_zero, Finsupp.coe_zero