awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible D
inst_8 : Invertible (fromBlocks A B C D)
this_1 : Invertible (α := Matrix n n α) 1 := invertibleOne
this : Invertible (α := Matrix m m α) 1 := invertibleOne
iDC : Invertible (α := Matrix (m ⊕ n) (m ⊕ n) α)
  (fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1) :=
  fromBlocksZero₁₂Invertible 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1
iBD : Invertible (α := Matrix (m ⊕ n) (m ⊕ n) α)
  (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1) :=
  fromBlocksZero₂₁Invertible 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 1
iBDC : Invertible
  (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
      fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D *
    fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1) :=
  inst_8.copy
    (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
        fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D *
      fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1)
    ⋯
refine :
  Invertible
    (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
      fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)
⊢ Invertible (fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)

Tactic:
refine (iBD.mulLeft _).symm ?_

Premises used: Equiv.symm, Invertible.mulLeft, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible D
inst_8 : Invertible (fromBlocks A B C D)
this_1 : Invertible (α := Matrix n n α) 1 := invertibleOne
this : Invertible (α := Matrix m m α) 1 := invertibleOne
iDC : Invertible (α := Matrix (m ⊕ n) (m ⊕ n) α)
  (fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1) :=
  fromBlocksZero₁₂Invertible 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1
iBD : Invertible (α := Matrix (m ⊕ n) (m ⊕ n) α)
  (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1) :=
  fromBlocksZero₂₁Invertible 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 1
iBDC : Invertible
  (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
      fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D *
    fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1) :=
  inst_8.copy
    (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
        fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D *
      fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1)
    ⋯
⊢ Invertible
    (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
      fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)

Tactic:
exact (iDC.mulRight _).symm iBDC

Premises used: Invertible.mulRight, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible A
inst_8 : Invertible (fromBlocks A B C D)
iABCD' : Invertible (α := Matrix (n ⊕ m) (n ⊕ m) α)
  ((fromBlocks A B C D).submatrix (⇑(Equiv.sumComm n m) : (a : n ⊕ m) → m ⊕ n)
    (⇑(Equiv.sumComm n m) : (a : n ⊕ m) → m ⊕ n)) :=
  (fromBlocks A B C D).submatrixEquivInvertible (Equiv.sumComm n m) (Equiv.sumComm n m)
iDCBA : Invertible (fromBlocks D C B A) := iABCD'.copy (fromBlocks D C B A) ⋯
⊢ Invertible (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)

Tactic:
exact invertibleOfFromBlocks₂₂Invertible D C B A

Premises used: Matrix.invertibleOfFromBlocks₂₂Invertible
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (invertibleEquivFromBlocks₂₂Invertible A B C D).nonempty_congr]

Premises used: Matrix.invertibleEquivFromBlocks₂₂Invertible, nonempty_invertible_iff_isUnit, Equiv.nonempty_congr
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 A
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (invertibleEquivFromBlocks₁₁Invertible A B C D).nonempty_congr]

Premises used: nonempty_invertible_iff_isUnit, Equiv.nonempty_congr, Matrix.invertibleEquivFromBlocks₁₁Invertible
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
haveI : ∀ (this : Invertible (α := Matrix m m α) 1), (fromBlocks 1 B C D).det = (D - C * B).det
⊢ (fromBlocks 1 B C D).det = (D - C * B).det

Tactic:
haveI : Invertible (1 : Matrix m m α) := invertibleOne
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible (α := Matrix m m α) 1
rw :
  det.{u_4, u_2} (n := m) 1 * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * B).det =
    (D - C * B).det
rw₁ : det.{u_4, u_2} (n := m) 1 * (D - C * 1 * B).det = (D - C * B).det
rw₂ : det.{u_4, u_2} (n := m) 1 * (D - C * B).det = (D - C * B).det
rw₃ : 1 * (D - C * B).det = (D - C * B).det
rw₄ rw₅ : (D - C * B).det = (D - C * B).det
⊢ (fromBlocks 1 B C D).det = (D - C * B).det

Tactic:
rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]

Premises used: invOf_one, Matrix.det_fromBlocks₁₁, Matrix.det_one, Matrix.mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
a :
  ∀ (i j : m ⊕ n),
    fromBlocks A B C D i j =
      (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) i j
⊢ 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)

Tactic:
ext (i j)
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
i j : m ⊕ n
a :
  ∀ (val : m),
    fromBlocks A B C D (Sum.inl val) j =
      (fromBlocks D C B A).submatrix (l := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inl val) j
a₁ :
  ∀ (val : n),
    fromBlocks A B C D (Sum.inr val) j =
      (fromBlocks D C B A).submatrix (l := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inr val) j
⊢ fromBlocks A B C D i j =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) i j

Tactic:
cases i
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
j : m ⊕ n
val : m
a :
  ∀ (val_1 : m),
    fromBlocks A B C D (Sum.inl val) (Sum.inl val_1) =
      (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : n),
    fromBlocks A B C D (Sum.inl val) (Sum.inr val_1) =
      (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inl val) (Sum.inr val_1)
⊢ fromBlocks A B C D (Sum.inl val) j =
    (fromBlocks D C B A).submatrix (l := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inl val) j

Tactic:
cases j
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
j : m ⊕ n
val : n
a :
  ∀ (val_1 : m),
    fromBlocks A B C D (Sum.inr val) (Sum.inl val_1) =
      (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : n),
    fromBlocks A B C D (Sum.inr val) (Sum.inr val_1) =
      (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
        (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inr val) (Sum.inr val_1)
⊢ fromBlocks A B C D (Sum.inr val) j =
    (fromBlocks D C B A).submatrix (l := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inr val) j

Tactic:
cases j
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
val val_1 : m
⊢ fromBlocks A B C D (Sum.inl val) (Sum.inl val_1) =
    (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inl val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
val : m
val_1 : n
⊢ fromBlocks A B C D (Sum.inl val) (Sum.inr val_1) =
    (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inl val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
val : n
val_1 : m
⊢ fromBlocks A B C D (Sum.inr val) (Sum.inl val_1) =
    (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inr val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
val val_1 : n
⊢ fromBlocks A B C D (Sum.inr val) (Sum.inr val_1) =
    (fromBlocks D C B A).submatrix (l := m ⊕ n) (o := m ⊕ n) (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m)
      (⇑(Equiv.sumComm m n) : (a : m ⊕ n) → n ⊕ m) (Sum.inr val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
⊢ 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)

Tactic:
have : fromBlocks A B C D =
      (fromBlocks D C B A).submatrix (Equiv.sumComm _ _) (Equiv.sumComm _ _) := by
    ext (i j)
    cases i <;> cases j <;> rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₂ rw₃ :
  D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).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

Tactic:
rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]

Premises used: Matrix.det_fromBlocks₁₁, Matrix.det_submatrix_equiv_self
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 α
haveI : ∀ (this : Invertible (α := Matrix n n α) 1), (fromBlocks A B C 1).det = (A - B * C).det
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
haveI : Invertible (1 : Matrix n n α) := invertibleOne
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₄ rw₅ : (A - B * C).det = (A - B * C).det
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]

Premises used: invOf_one, Matrix.det_fromBlocks₂₂, Matrix.det_one, Matrix.mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₂ rw₃ : (1 + A * B).det = (1 + A * B).det
⊢ (1 + A * B).det = (fromBlocks 1 (-A) B 1).det

Tactic:
rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]

Premises used: Matrix.det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₂ rw₃ : (1 + B * A).det = (1 + B * A).det
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det

Tactic:
rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]

Premises used: Matrix.mul_neg, Matrix.det_fromBlocks_one₁₁, sub_neg_eq_add
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₂ rw₃ : (B * A + 1).det = (B * A + 1).det
⊢ (A * B + 1).det = (B * A + 1).det

Tactic:
rw [add_comm, det_one_add_mul_comm, add_comm]

Premises used: add_comm, Matrix.det_one_add_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₄ rw₅ : (1 - B * A).det = (1 - B * A).det
⊢ (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]

Premises used: sub_eq_add_neg, Matrix.mul_neg, Matrix.neg_mul, Matrix.det_one_add_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rw₅ rw₆ : 1 + v ⬝ᵥ u = 1 + v ⬝ᵥ u
⊢ (1 + replicateCol ι u * replicateRow ι v).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]

Premises used: Pi.add_apply, Matrix.replicateRow_mul_replicateCol_apply, Matrix.one_apply_eq, Matrix.det_unique, Matrix.det_one_add_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 → α
nth_rewrite :
  (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
⊢ (A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Tactic:
nth_rewrite 1 [← Matrix.mul_one A]

Premises used: Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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
rwa₈ :
  A.det * (1 + replicateRow ι v * (A⁻¹ * replicateCol ι u)).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₉ : IsUnit A.det
rwa₁₀ :
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁₁ : IsUnit A.det
rwa₁₂ :
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁₃ rwa₁₄ rwa₁₅ : IsUnit A.det
⊢ (A * 1 + 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]

Premises used: HMul.hMul, Matrix.mul_assoc, Matrix.replicateCol, Matrix.det_mul, Matrix.mul_add, Matrix.mul_nonsing_inv_cancel_left, Matrix.replicateRow, Matrix.det_one_add_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
nth_rewrite : (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
⊢ (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Tactic:
nth_rewrite 1 [← Matrix.mul_one A]

Premises used: Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁ : IsUnit A.det
rwa₂ : (A * (1 + A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₃ : IsUnit A.det
rwa₄ : A.det * (1 + A⁻¹ * (U * V)).det = A.det * (1 + V * A⁻¹ * U).det
rwa₅ : IsUnit A.det
rwa₆ : A.det * (1 + A⁻¹ * U * V).det = A.det * (1 + V * A⁻¹ * U).det
rwa₇ : IsUnit A.det
rwa₈ : A.det * (1 + V * (A⁻¹ * U)).det = A.det * (1 + V * A⁻¹ * U).det
rwa₉ : IsUnit A.det
rwa₁₀ : A.det * (1 + V * A⁻¹ * U).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁₁ : IsUnit A.det
rwa₁₂ : A.det * (1 + V * A⁻¹ * U).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁₃ rwa₁₄ rwa₁₅ : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Tactic:
rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]

Premises used: HMul.hMul, Matrix.mul_assoc, Matrix.det_mul, Matrix.mul_add, Matrix.mul_nonsing_inv_cancel_left, Matrix.det_one_add_mul_comm