awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val : Invertible A
pos : ∀ (val : Invertible D), (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
cases hD.nonempty_invertible

Premises used: IsUnit.nonempty_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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val : Invertible A
val_1 : Invertible D
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
pos :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _ =
    fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
      0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₂₁_eq]

Premises used: Matrix.invOf_eq_nonsing_inv, Matrix.invOf_fromBlocks_zero₂₁_eq
-- 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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
⊢ ¬IsUnit D

Tactic:
have hD := hAD.not.mp hA
-- 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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
⊢ ¬IsUnit (fromBlocks A B 0 D)

Tactic:
have : ¬IsUnit (fromBlocks A B 0 D) :=
      isUnit_fromBlocks_zero₂₁.not.mpr (not_and'.mpr fun _ => hA)
-- 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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
neg :
  Ring.inverse (fromBlocks A B 0 D) =
    fromBlocks (Ring.inverse A) (-(Ring.inverse A * B * Ring.inverse D)) 0 (Ring.inverse D)
neg₁ : Ring.inverse (fromBlocks A B 0 D) = fromBlocks 0 (-(0 * B * Ring.inverse D)) 0 (Ring.inverse D)
neg₂ : Ring.inverse (fromBlocks A B 0 D) = fromBlocks 0 (-(0 * B * 0)) 0 0
neg₃ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 (-(0 * B * 0)) 0 0)
neg₄ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 (-0) 0 0)
neg₅ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 0 0)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
      Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]

Premises used: Matrix.nonsing_inv_eq_ringInverse, Ring.inverse_non_unit, Matrix.zero_mul, Matrix.fromBlocks_zero, neg_zero
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
pos : ∀ (hA : IsUnit A), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
neg : ∀ (hA : ¬IsUnit A), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
by_cases hA : IsUnit A

Premises used: IsUnit
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
⊢ IsUnit D

Tactic:
have hD := hAD.mp hA
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
pos : ∀ (val : Invertible A), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
cases hA.nonempty_invertible

Premises used: IsUnit.nonempty_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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val : Invertible A
pos : ∀ (val : Invertible D), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
cases hD.nonempty_invertible

Premises used: IsUnit.nonempty_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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val : Invertible A
val_1 : Invertible D
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
pos :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _ =
    fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 0
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₁₂_eq]

Premises used: Matrix.invOf_eq_nonsing_inv, Matrix.invOf_fromBlocks_zero₁₂_eq
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
⊢ ¬IsUnit D

Tactic:
have hD := hAD.not.mp hA
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
⊢ ¬IsUnit (fromBlocks A 0 C D)

Tactic:
have : ¬IsUnit (fromBlocks A 0 C D) :=
      isUnit_fromBlocks_zero₁₂.not.mpr (not_and'.mpr fun _ => hA)
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
neg :
  Ring.inverse (fromBlocks A 0 C D) =
    fromBlocks (Ring.inverse A) 0 (-(Ring.inverse D * C * Ring.inverse A)) (Ring.inverse D)
neg₁ : Ring.inverse (fromBlocks A 0 C D) = fromBlocks 0 0 (-(Ring.inverse D * C * 0)) (Ring.inverse D)
neg₂ : Ring.inverse (fromBlocks A 0 C D) = fromBlocks 0 0 (-(0 * C * 0)) 0
neg₃ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 (-(0 * C * 0)) 0)
neg₄ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 (-0) 0)
neg₅ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 0 0)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
      Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]

Premises used: Matrix.nonsing_inv_eq_ringInverse, Ring.inverse_non_unit, Matrix.zero_mul, Matrix.fromBlocks_zero, neg_zero
-- 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 (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
convert_1 :
  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)
convert_6 : Invertible D
convert_7 :
  fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ +
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne
      (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 A B C D)

Tactic:
convert!
    Invertible.copy' _ _
      (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D))
        (-(⅟D * C * ⅟(A - B * ⅟D * C))) (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D))
      (fromBlocks_eq_of_invertible₂₂ _ _ _ _) _

Premises used: Matrix.fromBlocks, HMul.hMul, Invertible.copy', HSub.hSub, Invertible.invOf, Matrix.fromBlocks_eq_of_invertible₂₂, HAdd.hAdd, Neg.neg
-- 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 (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
this_1 : Invertible (α := Matrix n n α) 1 := invertibleOne
this : Invertible (α := Matrix m m α) 1 := invertibleOne
convert_1 :
  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 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)

Tactic:
refine Invertible.mul ?_ (fromBlocksZero₁₂Invertible _ _ _)

Premises used: Invertible.mul
-- 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 (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
this_1 : Invertible (α := Matrix n n α) 1 := invertibleOne
this : Invertible (α := Matrix m m α) 1 := invertibleOne
⊢ 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
      Invertible.mul (fromBlocksZero₂₁Invertible _ _ _)
        (fromBlocksZero₂₁Invertible _ _ _)

Premises used: Invertible.mul
-- 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 (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
⊢ fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ +
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) =
    fromBlocks 1 0 (-(1 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) * 1)) 1 *
      (fromBlocks
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
          (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
                0 *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
          0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        fromBlocks 1 (-(1 * (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) * 1)) 0 1)

Tactic:
simp only [fromBlocks_multiply, Matrix.one_mul, Matrix.mul_one, Matrix.zero_mul,
      Matrix.mul_zero, add_zero, zero_add, neg_zero, Matrix.mul_neg, Matrix.neg_mul, neg_neg, ←
      Matrix.mul_assoc, add_comm (⅟D)]

Premises used: Matrix.mul_assoc, Invertible.invOf, Matrix.mul_neg, neg_neg, Matrix.mul_zero, zero_add, add_comm, Matrix.zero_mul, Matrix.mul_one, Matrix.neg_mul, Matrix.fromBlocks_multiply, add_zero, neg_zero, Matrix.one_mul
-- 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 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)
this : Invertible (fromBlocks D C B A) := D.fromBlocks₂₂Invertible C B A
iDCBA : Invertible (α := Matrix (m ⊕ 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)) :=
  (fromBlocks D C B A).submatrixEquivInvertible (Equiv.sumComm m n) (Equiv.sumComm m n)
⊢ Invertible (fromBlocks A B C D)

Tactic:
exact
    iDCBA.copy' _
      (fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
        (-(⅟(D - C * ⅟A * B) * C * ⅟A)) (⅟(D - C * ⅟A * B)))
      (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm
      (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm

Premises used: Matrix.fromBlocks, HMul.hMul, Invertible.copy', Matrix.fromBlocks_submatrix_sum_swap_sum_swap, HSub.hSub, Invertible.invOf, HAdd.hAdd, Eq.symm, Neg.neg
-- 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
inst_6 : Invertible (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
inst_7 : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₂₂Invertible B C D
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B C D) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B C D) _

Tactic:
(rfl : ⅟(fromBlocks A B C D) = _)

Premises used: 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
inst_6 : Invertible (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
inst_7 : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₂₂Invertible B C D
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B C D) _ =
    fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ +
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _)

Tactic:
convert! (rfl : ⅟(fromBlocks A B C D) = _)

Premises used: 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 A
inst_6 : Invertible (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)
inst_7 : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₁₁Invertible B C D
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B C D) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B C D) _

Tactic:
(rfl : ⅟(fromBlocks A B C D) = _)

Premises used: 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 A
inst_6 : Invertible (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)
inst_7 : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₁₁Invertible B C D
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B C D) _ =
    fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) _ *
            C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) _))
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) _ *
            C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) _)

Tactic:
convert! (rfl : ⅟(fromBlocks A B C D) = _)

Premises used: rfl
-- 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 : Invertible (fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)
⊢ Invertible (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)

Tactic:
exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1

Premises used: HMul.hMul, HSub.hSub, Invertible.invOf, Matrix.invertibleOfFromBlocksZero₁₂Invertible, Prod.fst, OfNat.ofNat
-- 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)
suffices : Invertible (fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)
⊢ Invertible (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)

Tactic:
suffices Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D) by
    exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1