awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
this :
  fromBlocks A B C D =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
⊢ (fromBlocks A B C D).det = D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
have rw : det (n := m ⊕ n)
    ((fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)) =
  D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
Tactic: rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
this :
  fromBlocks A B C D =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
rw :
  det (n := m ⊕ n)
      ((fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)) =
    D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
⊢ (fromBlocks A B C D).det = D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
have rw₁ : (fromBlocks D C B A).det = D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
Tactic: rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
this :
  fromBlocks A B C D =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
rw :
  det (n := m ⊕ n)
      ((fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)) =
    D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
rw₁ : (fromBlocks D C B A).det = D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
⊢ (fromBlocks A B C D).det = D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
have rw₂ : D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det =
  D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
Tactic: rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
⊢ (fromBlocks A B C 1).det = (A - B * C).det
have haveI : ∀ (this : Invertible (α := Matrix n n α) 1), (fromBlocks A B C 1).det = (A - B * C).det
Tactic: haveI : Invertible (1 : Matrix n n α) := invertibleOne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible (α := Matrix n n α) 1
⊢ (fromBlocks A B C 1).det = (A - B * C).det
have rw : det.{u_4, u_3} (n := n) 1 * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * C).det =
  (A - B * C).det
Tactic: rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible (α := Matrix n n α) 1
rw :
  det.{u_4, u_3} (n := n) 1 * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * C).det =
    (A - B * C).det
⊢ (fromBlocks A B C 1).det = (A - B * C).det
have rw₁ : det.{u_4, u_3} (n := n) 1 * (A - B * 1 * C).det = (A - B * C).det
Tactic: rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible (α := Matrix n n α) 1
rw :
  det.{u_4, u_3} (n := n) 1 * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * C).det =
    (A - B * C).det
rw₁ : det.{u_4, u_3} (n := n) 1 * (A - B * 1 * C).det = (A - B * C).det
⊢ (fromBlocks A B C 1).det = (A - B * C).det
have rw₂ : det.{u_4, u_3} (n := n) 1 * (A - B * C).det = (A - B * C).det
Tactic: rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible (α := Matrix n n α) 1
rw :
  det.{u_4, u_3} (n := n) 1 * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * C).det =
    (A - B * C).det
rw₁ : det.{u_4, u_3} (n := n) 1 * (A - B * 1 * C).det = (A - B * C).det
rw₂ : det.{u_4, u_3} (n := n) 1 * (A - B * C).det = (A - B * C).det
⊢ (fromBlocks A B C 1).det = (A - B * C).det
have rw₃ : 1 * (A - B * C).det = (A - B * C).det
Tactic: rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible (α := Matrix n n α) 1
rw :
  det.{u_4, u_3} (n := n) 1 * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * C).det =
    (A - B * C).det
rw₁ : det.{u_4, u_3} (n := n) 1 * (A - B * 1 * C).det = (A - B * C).det
rw₂ : det.{u_4, u_3} (n := n) 1 * (A - B * C).det = (A - B * C).det
rw₃ : 1 * (A - B * C).det = (A - B * C).det
⊢ (fromBlocks A B C 1).det = (A - B * C).det
have rw₄ : (A - B * C).det = (A - B * C).det
Tactic: rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + A * B).det = (fromBlocks 1 (-A) B 1).det
have rw : (1 + A * B).det = (1 - -A * B).det
Tactic: rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + A * B).det = (1 - -A * B).det
⊢ (1 + A * B).det = (fromBlocks 1 (-A) B 1).det
have rw₁ : (1 + A * B).det = (1 - -(A * B)).det
Tactic: rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + A * B).det = (1 - -A * B).det
rw₁ : (1 + A * B).det = (1 - -(A * B)).det
⊢ (1 + A * B).det = (fromBlocks 1 (-A) B 1).det
have rw₂ : (1 + A * B).det = (1 + A * B).det
Tactic: rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det
have rw : (1 - B * -A).det = (1 + B * A).det
Tactic: rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 - B * -A).det = (1 + B * A).det
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det
have rw₁ : (1 - -(B * A)).det = (1 + B * A).det
Tactic: rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 - B * -A).det = (1 + B * A).det
rw₁ : (1 - -(B * A)).det = (1 + B * A).det
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det
have rw₂ : (1 + B * A).det = (1 + B * A).det
Tactic: rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (A * B + 1).det = (B * A + 1).det
have rw : (1 + A * B).det = (B * A + 1).det
Tactic: rw [add_comm, det_one_add_mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + A * B).det = (B * A + 1).det
⊢ (A * B + 1).det = (B * A + 1).det
have rw₁ : (1 + B * A).det = (B * A + 1).det
Tactic: rw [add_comm, det_one_add_mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + A * B).det = (B * A + 1).det
rw₁ : (1 + B * A).det = (B * A + 1).det
⊢ (A * B + 1).det = (B * A + 1).det
have rw₂ : (B * A + 1).det = (B * A + 1).det
Tactic: rw [add_comm, det_one_add_mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - A * B).det = (1 - B * A).det
have rw : (1 + -(A * B)).det = (1 - B * A).det
Tactic: rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + -(A * B)).det = (1 - B * A).det
⊢ (1 - A * B).det = (1 - B * A).det
have rw₁ : (1 + -A * B).det = (1 - B * A).det
Tactic: rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + -(A * B)).det = (1 - B * A).det
rw₁ : (1 + -A * B).det = (1 - B * A).det
⊢ (1 - A * B).det = (1 - B * A).det
have rw₂ : (1 + B * -A).det = (1 - B * A).det
Tactic: rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + -(A * B)).det = (1 - B * A).det
rw₁ : (1 + -A * B).det = (1 - B * A).det
rw₂ : (1 + B * -A).det = (1 - B * A).det
⊢ (1 - A * B).det = (1 - B * A).det
have rw₃ : (1 + -(B * A)).det = (1 - B * A).det
Tactic: rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m n α
B : Matrix n m α
rw : (1 + -(A * B)).det = (1 - B * A).det
rw₁ : (1 + -A * B).det = (1 - B * A).det
rw₂ : (1 + B * -A).det = (1 - B * A).det
rw₃ : (1 + -(B * A)).det = (1 - B * A).det
⊢ (1 - A * B).det = (1 - B * A).det
have rw₄ : (1 - B * A).det = (1 - B * A).det
Tactic: rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
u v : m → α
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u
have rw : (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
Tactic: rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
u v : m → α
rw : (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u
have rw₁ : HAdd.hAdd (α := Matrix ι ι α) 1 (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
Tactic: rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
u v : m → α
rw : (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
rw₁ : HAdd.hAdd (α := Matrix ι ι α) 1 (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u
have rw₂ : HAdd.hAdd (α := ι → α) (1 default) ((replicateRow ι v * replicateCol ι u) default) default = 1 + v ⬝ᵥ u
Tactic: rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
u v : m → α
rw : (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
rw₁ : HAdd.hAdd (α := Matrix ι ι α) 1 (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
rw₂ : HAdd.hAdd (α := ι → α) (1 default) ((replicateRow ι v * replicateCol ι u) default) default = 1 + v ⬝ᵥ u
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u
have rw₃ : 1 default default + (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
Tactic: rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
u v : m → α
rw : (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
rw₁ : HAdd.hAdd (α := Matrix ι ι α) 1 (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
rw₂ : HAdd.hAdd (α := ι → α) (1 default) ((replicateRow ι v * replicateCol ι u) default) default = 1 + v ⬝ᵥ u
rw₃ : 1 default default + (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u
have rw₄ : 1 + (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
Tactic: rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
u v : m → α
rw : (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
rw₁ : HAdd.hAdd (α := Matrix ι ι α) 1 (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
rw₂ : HAdd.hAdd (α := ι → α) (1 default) ((replicateRow ι v * replicateCol ι u) default) default = 1 + v ⬝ᵥ u
rw₃ : 1 default default + (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
rw₄ : 1 + (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u
have rw₅ : 1 + v ⬝ᵥ u = 1 + v ⬝ᵥ u
Tactic: rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have nth_rewrite : (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: nth_rewrite 1 [← Matrix.mul_one A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have rwa : (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
rwa :
  (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁ : IsUnit A.det
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have rwa₂ : (A * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
rwa :
  (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁ : IsUnit A.det
rwa₂ :
  (A * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₃ : IsUnit A.det
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have rwa₄ : A.det * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v)).det =
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
rwa :
  (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁ : IsUnit A.det
rwa₂ :
  (A * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₃ : IsUnit A.det
rwa₄ :
  A.det * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v)).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₅ : IsUnit A.det
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have rwa₆ : A.det * (1 + A⁻¹ * replicateCol ι u * replicateRow ι v).det =
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
rwa :
  (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁ : IsUnit A.det
rwa₂ :
  (A * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₃ : IsUnit A.det
rwa₄ :
  A.det * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v)).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₅ : IsUnit A.det
rwa₆ :
  A.det * (1 + A⁻¹ * replicateCol ι u * replicateRow ι v).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₇ : IsUnit A.det
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have rwa₈ : A.det * (1 + replicateRow ι v * (A⁻¹ * replicateCol ι u)).det =
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]