awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
this : (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D
rw :
  Matrix.det.{u_6, u_7} (n := m ⊕ n) ((toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e) =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
rw₁ :
  (fromBlocks A B 0 D).det =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
rw₂ :
  (fromBlocks A B 0 D).det =
    HMul.hMul (α := R) (β := R)
      (Matrix.det.{u_6, u_7} (n := m) ((toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)
rw₃ :
  (fromBlocks A B 0 D).det =
    HMul.hMul (α := R)
      (Matrix.det.{u_6, u_7} (n := m) ((toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)))
      (Matrix.det.{u_6, u_7} (n := n) ((toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)))
rw₄ rw₅ :
  A.det * D.det =
    HMul.hMul (α := R)
      (Matrix.det.{u_6, u_7} (n := m) ((toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)))
      (Matrix.det.{u_6, u_7} (n := n) ((toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)))
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) e =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)

Tactic:
rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]

Premises used: Matrix.det_fromBlocks_zero₂₁, LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
suffices : (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) e =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : ↥W →ₗ[R] ↥W) → R) (e.restrict he) : R)
      ((LinearMap.det : (a : V ⧸ W →ₗ[R] V ⧸ W) → R) (W.mapQ W e he) : R)

Tactic:
suffices LinearMap.toMatrix b b e = Matrix.fromBlocks A B 0 D by
    rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
a : ∀ (u v : m ⊕ n), (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e u v = fromBlocks A B 0 D u v
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D

Tactic:
ext u v
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
i k : m
⊢ Eq.{u_6 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V)) :
            Finsupp.{u_7, u_6} (m ⊕ n) R) :
          (a : m ⊕ n) → R)
        (Sum.inl i) :
      R)
    ((((bW.repr : (a : ↥W) → m →₀ R) ((e.restrict he : (a : ↥W) → ↥W) ((bW : (a : m) → ↥W) k)) : m →₀ R) : (a : m) → R)
        i :
      R)

Tactic:
apply sumQuot_repr_inl_of_mem

Premises used: Module.Basis.sumQuot_repr_inl_of_mem
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
i : m
l : n
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) (Sum.inr l) =
    fromBlocks A B 0 D (Sum.inl i) (Sum.inr l)

Tactic:
simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]

Premises used: Matrix.fromBlocks_apply₁₂, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
v : m ⊕ n
i : m
a :
  ∀ (k : m),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) (Sum.inl k) =
      fromBlocks A B 0 D (Sum.inl i) (Sum.inl k)
a₁ :
  ∀ (l : n),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) (Sum.inr l) =
      fromBlocks A B 0 D (Sum.inl i) (Sum.inr l)
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) v = fromBlocks A B 0 D (Sum.inl i) v

Tactic:
cases v with
    | inl k =>
      simp only [b, sumQuot_inl, Matrix.fromBlocks_apply₁₁, A, LinearMap.toMatrix_apply]
      apply sumQuot_repr_inl_of_mem
    | inr l => simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]

Premises used: Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, LinearMap.inl, Module.Basis.sumQuot_repr_inl_of_mem, LinearMap.inr, Module.Basis.sumQuot_inl, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j : n
k : m
this :
  Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V)) : V ⧸ W) (0 : V ⧸ W)
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) (Sum.inl k) =
    fromBlocks A B 0 D (Sum.inr j) (Sum.inl k)

Tactic:
simp [LinearMap.toMatrix_apply, b, this]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j : n
k : m
a : Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V)) : V ⧸ W) (0 : V ⧸ W)
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) (Sum.inl k) =
    fromBlocks A B 0 D (Sum.inr j) (Sum.inl k)

Tactic:
suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j : n
k : m
a : Membership.mem (α := V) W ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V) : V)
⊢ Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V)) : V ⧸ W) (0 : V ⧸ W)

Tactic:
rw [← LinearMap.mem_ker, Submodule.ker_mkQ]

Premises used: LinearMap.mem_ker, Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j : n
k : m
⊢ Membership.mem (α := V) W ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V) : V)

Tactic:
he (Submodule.coe_mem (bW k))

Premises used: Set.Mem, setOf, Submodule.coe_mem, Set.preimage, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j : n
k : m
⊢ Membership.mem (α := V) W ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V) : V)

Tactic:
exact he (Submodule.coe_mem (bW k))

Premises used: Submodule.coe_mem, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j l : n
a :
  Eq.{u_6 + 1} (α := R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R)
              ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V))) :
            n →₀ R) :
          (a : n) → R)
        j :
      R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R) ((W.mapQ W e he : (a : V ⧸ W) → V ⧸ W) ((bQ : (a : n) → V ⧸ W) l)) : n →₀ R) :
          (a : n) → R)
        j :
      R)
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) (Sum.inr l) =
    fromBlocks A B 0 D (Sum.inr j) (Sum.inr l)

Tactic:
simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]

Premises used: Matrix.fromBlocks_apply₂₂, LinearMap.toMatrix_apply, Module.Basis.sumQuot_repr_inr
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j l : n
a :
  Eq.{u_6 + 1} (α := R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R)
              ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V))) :
            n →₀ R) :
          (a : n) → R)
        j :
      R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R)
              (Submodule.Quotient.mk ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V))) :
            n →₀ R) :
          (a : n) → R)
        j :
      R)
⊢ Eq.{u_6 + 1} (α := R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R)
              ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V))) :
            n →₀ R) :
          (a : n) → R)
        j :
      R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R) ((W.mapQ W e he : (a : V ⧸ W) → V ⧸ W) ((bQ : (a : n) → V ⧸ W) l)) : n →₀ R) :
          (a : n) → R)
        j :
      R)

Tactic:
rw [← sumQuot_inr bW bQ l, W.mapQ_apply]

Premises used: Submodule.mapQ_apply, Module.Basis.sumQuot_inr
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
j l : n
⊢ Eq.{u_6 + 1} (α := R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R)
              ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V))) :
            n →₀ R) :
          (a : n) → R)
        j :
      R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R)
              (Submodule.Quotient.mk ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V))) :
            n →₀ R) :
          (a : n) → R)
        j :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
v : m ⊕ n
j : n
a :
  ∀ (k : m),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) (Sum.inl k) =
      fromBlocks A B 0 D (Sum.inr j) (Sum.inl k)
a₁ :
  ∀ (l : n),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) (Sum.inr l) =
      fromBlocks A B 0 D (Sum.inr j) (Sum.inr l)
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) v = fromBlocks A B 0 D (Sum.inr j) v

Tactic:
cases v with
    | inl k =>
      suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))
    | inr l =>
      simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
      rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
      simp

Premises used: Submodule.mapQ_apply, Matrix.fromBlocks_apply₂₂, LinearMap.inl, LinearMap.mem_ker, Submodule.ker_mkQ, LinearMap.inr, LinearMap.toMatrix_apply, Module.Basis.sumQuot_repr_inr