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 α
inst_5 : Invertible A
inst_6 : Invertible D
inst_7 : Invertible (fromBlocks A B 0 D)
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _

Tactic:
(rfl : ⅟(fromBlocks A B 0 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 α
D : Matrix n n α
inst_5 : Invertible A
inst_6 : Invertible D
inst_7 : Invertible (fromBlocks A B 0 D)
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ @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 _)

Tactic:
convert! (rfl : ⅟(fromBlocks A B 0 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 α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible A
inst_6 : Invertible D
inst_7 : Invertible (fromBlocks A 0 C D)
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _

Tactic:
(rfl : ⅟(fromBlocks A 0 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 α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible A
inst_6 : Invertible D
inst_7 : Invertible (fromBlocks A 0 C D)
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
⊢ @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:
convert! (rfl : ⅟(fromBlocks A 0 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 α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A B 0 D)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _ * fromBlocks A B 0 D = 1

Tactic:
have := invOf_mul_self (fromBlocks A B 0 D)
-- 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 α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A B 0 D)
this : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _ * fromBlocks A B 0 D = 1
⊢ fromBlocks
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₂ * 0)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ * B +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₂ * D)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂ * 0)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₁ * B +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂ * D) =
    1

Tactic:
rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this

Premises used: Matrix.fromBlocks, Matrix.fromBlocks_toBlocks, Invertible.invOf, Matrix.fromBlocks_multiply, 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 α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₂ * 0)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ * B +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₂ * D)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂ * 0)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₁ * B +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂ * D) =
    1
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ * A = 1

Tactic:
simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.mul_zero, add_zero, ← fromBlocks_one] using
        congr_arg Matrix.toBlocks₁₁ this

Premises used: Matrix.mul_zero, congr_arg, Matrix.toBlocks_fromBlocks₁₁, Matrix.fromBlocks_one, Matrix.toBlocks₁₁, add_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 α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A B 0 D)
⊢ fromBlocks A B 0 D * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _ = 1

Tactic:
have := mul_invOf_self (fromBlocks A B 0 D)
-- 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 α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks
      (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ +
        B * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₁)
      (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₂ +
        B * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂)
      (0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ +
        D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₁)
      (0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₂ +
        D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂) =
    1
⊢ D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂ = 1

Tactic:
simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.zero_mul, zero_add, ← fromBlocks_one] using
        congr_arg Matrix.toBlocks₂₂ this

Premises used: zero_add, congr_arg, Matrix.fromBlocks_one, Matrix.toBlocks₂₂, Matrix.zero_mul, Matrix.toBlocks_fromBlocks₂₂
-- 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
⊢ fromBlocks A 0 C D * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _ = 1

Tactic:
have := mul_invOf_self (fromBlocks A 0 C D)
-- 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
this : fromBlocks A 0 C D * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _ = 1
⊢ fromBlocks
      (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
        0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
      (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
        0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂)
      (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
        D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
      (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
        D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂) =
    1

Tactic:
rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this

Premises used: Matrix.fromBlocks, Matrix.fromBlocks_toBlocks, Invertible.invOf, Matrix.fromBlocks_multiply, 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks
      (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
        0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
      (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
        0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂)
      (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
        D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
      (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
        D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂) =
    1
⊢ (fromBlocks
        (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
          0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
        (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
          0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂)
        (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
          D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
        (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
          D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂)).toBlocks₁₁ =
    toBlocks₁₁.{u_2, u_3, u_2, u_3, u_4} (m := n) (o := n) 1

Tactic:
replace := congr_arg Matrix.toBlocks₁₁ this
-- 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks
        (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
          0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
        (A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
          0 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂)
        (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ +
          D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁)
        (C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ +
          D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂)).toBlocks₁₁ =
    toBlocks₁₁.{u_2, u_3, u_2, u_3, u_4} (m := n) (o := n) 1
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ = 1

Tactic:
simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.zero_mul, add_zero, ← fromBlocks_one] using
        this

Premises used: Matrix.toBlocks_fromBlocks₁₁, Matrix.fromBlocks_one, Matrix.zero_mul, add_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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _ * fromBlocks A 0 C D = 1

Tactic:
have := invOf_mul_self (fromBlocks A 0 C D)
-- 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
this : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _ * fromBlocks A 0 C D = 1
⊢ fromBlocks
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * C)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * 0 +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * D)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * C)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * 0 +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D) =
    1

Tactic:
rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this

Premises used: Matrix.fromBlocks, Matrix.fromBlocks_toBlocks, Invertible.invOf, Matrix.fromBlocks_multiply, 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * C)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * 0 +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * D)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * A +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * C)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * 0 +
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D) =
    1
⊢ (fromBlocks
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * A +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * C)
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * 0 +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * D)
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * A +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * C)
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * 0 +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D)).toBlocks₂₂ =
    toBlocks₂₂.{u_2, u_3, u_2, u_3, u_4} (l := m) (n := m) 1

Tactic:
replace := congr_arg Matrix.toBlocks₂₂ this
-- 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 α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * A +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * C)
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ * 0 +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₂ * D)
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * A +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * C)
        ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₁ * 0 +
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D)).toBlocks₂₂ =
    toBlocks₂₂.{u_2, u_3, u_2, u_3, u_4} (l := m) (n := m) 1
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D = 1

Tactic:
simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.mul_zero, zero_add, ← fromBlocks_one] using
        this

Premises used: Matrix.mul_zero, zero_add, Matrix.fromBlocks_one, Matrix.toBlocks_fromBlocks₂₂
-- 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 α
D : Matrix n n α
i : Invertible A × Invertible D
this_1 : Invertible A := i.1
this : Invertible D := i.2
⊢ Invertible (fromBlocks A B 0 D)

Tactic:
exact fromBlocksZero₂₁Invertible A B D

Premises used: Matrix.fromBlocksZero₂₁Invertible
-- 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 α
C : Matrix n m α
D : Matrix n n α
i : Invertible A × Invertible D
this_1 : Invertible A := i.1
this : Invertible D := i.2
⊢ Invertible (fromBlocks A 0 C D)

Tactic:
exact fromBlocksZero₁₂Invertible A C D

Premises used: Matrix.fromBlocksZero₁₂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 α
⊢ IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D

Tactic:
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod,
    (fromBlocksZero₂₁InvertibleEquiv _ _ _).nonempty_congr]

Premises used: nonempty_prod, Matrix.fromBlocksZero₂₁InvertibleEquiv, 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 α
C : Matrix n m α
D : Matrix n n α
⊢ IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D

Tactic:
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod,
    (fromBlocksZero₁₂InvertibleEquiv _ _ _).nonempty_congr]

Premises used: nonempty_prod, nonempty_invertible_iff_isUnit, Equiv.nonempty_congr, Matrix.fromBlocksZero₁₂InvertibleEquiv
-- 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
pos : ∀ (hA : IsUnit A), (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
neg : ∀ (hA : ¬IsUnit A), (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:
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 α
B : Matrix m n α
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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
pos : ∀ (val : Invertible A), (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 hA.nonempty_invertible

Premises used: IsUnit.nonempty_invertible