awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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)
have 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)
Tactic: rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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)
have 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)))
Tactic: rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)))
⊢ (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)
have 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)))
Tactic: rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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)
have suffices : (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D
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₂₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e = fromBlocks A B 0 D
have 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
Tactic: ext u v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (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
have 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)
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]
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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
have 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)
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]
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (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)
have 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)
Tactic: suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V)) : V ⧸ W) (0 : V ⧸ W)
have a : Membership.mem (α := V) W ((e : (a : V) → V) (↑((bW : (a : m) → ↥W) k) : V) : V)
Tactic: rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (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)
have 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)
Tactic: simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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) ((W.mapQ W e he : (a : V ⧸ W) → V ⧸ W) ((bQ : (a : n) → V ⧸ W) l)) : n →₀ R) :
          (a : n) → R)
        j :
      R)
have 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)
Tactic: rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (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
have 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)
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
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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
have 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)
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
Cleared hypotheses: v