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 α
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
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg₃ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 (-(0 * B * 0)) 0 0)
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]
-- 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 α
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)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg₄ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 (-0) 0 0)
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]
-- 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 α
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)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg₅ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 0 0)
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]
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have pos : ∀ (hA : IsUnit A), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
Tactic: by_cases hA : IsUnit A
-- 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 α
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⁻¹
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg : ∀ (hA : ¬IsUnit A), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
Tactic: by_cases hA : IsUnit A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have hD : IsUnit D
Tactic: have hD := hAD.mp hA
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have pos : ∀ (val : Invertible A), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
Tactic: cases hA.nonempty_invertible
-- 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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val : Invertible A
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have pos : ∀ (val : Invertible D), (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
Tactic: cases hD.nonempty_invertible
-- 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 α
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
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have 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 _)
Tactic: simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₁₂_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have hD : ¬IsUnit D
Tactic: have hD := hAD.not.mp hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have this : ¬IsUnit (fromBlocks A 0 C D)
Tactic: have : ¬IsUnit (fromBlocks A 0 C D) :=
      isUnit_fromBlocks_zero₁₂.not.mpr (not_and'.mpr fun _ => hA)
-- 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 α
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)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg : Ring.inverse (fromBlocks A 0 C D) =
  fromBlocks (Ring.inverse A) 0 (-(Ring.inverse D * C * Ring.inverse A)) (Ring.inverse 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]
-- 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 α
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)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg₁ : Ring.inverse (fromBlocks A 0 C D) = fromBlocks 0 0 (-(Ring.inverse D * C * 0)) (Ring.inverse 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]
-- 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 α
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)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg₂ : Ring.inverse (fromBlocks A 0 C D) = fromBlocks 0 0 (-(0 * C * 0)) 0
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]
-- 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 α
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
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg₃ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 (-(0 * C * 0)) 0)
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]
-- 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 α
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)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg₄ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 (-0) 0)
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]
-- 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 α
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)
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
have neg₅ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α) 0 (fromBlocks 0 0 0 0)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
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)
⊢ Invertible (fromBlocks A B C D)
have 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)
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₂₂ _ _ _ _) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
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
⊢ Invertible (fromBlocks A B C D)
have 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)
    _
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₂₂ _ _ _ _) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
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 *
      fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1)
have 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)
Tactic: refine Invertible.mul ?_ (fromBlocksZero₁₂Invertible _ _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
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)
⊢ Invertible (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
have suffices : Invertible (fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)
Tactic: suffices Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D) by
    exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
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 (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)
have refine : Invertible
  (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
    fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D)
Tactic: refine (iBD.mulLeft _).symm ?_
-- 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 A
⊢ (fromBlocks A B C D).det = A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
have rw : (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1 *
        fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) *
      fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1).det =
  A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
Tactic: rw [fromBlocks_eq_of_invertible₁₁ (A := A), det_mul, det_mul, det_fromBlocks_zero₂₁,
    det_fromBlocks_zero₂₁, det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]
-- 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 A
rw :
  (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1 *
          fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) *
        fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1).det =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
⊢ (fromBlocks A B C D).det = A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
have rw₁ : (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1 *
        fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)).det *
    det (fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1) =
  A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
Tactic: rw [fromBlocks_eq_of_invertible₁₁ (A := A), det_mul, det_mul, det_fromBlocks_zero₂₁,
    det_fromBlocks_zero₂₁, det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]