awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible 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
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
⊢ (fromBlocks A B C D).det = A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
have rw₂ : det (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]
-- 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
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
rw₂ :
  det (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
⊢ (fromBlocks A B C D).det = A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
have rw₃ : det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
      (A.det * (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]
-- 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
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
rw₂ :
  det (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
rw₃ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (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
⊢ (fromBlocks A B C D).det = A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
have rw₄ : det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
      (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
    HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 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]
-- 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
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
rw₂ :
  det (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
rw₃ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (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
rw₄ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) =
    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₅ : HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) *
      (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
    HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 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]
-- 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
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
rw₂ :
  det (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
rw₃ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (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
rw₄ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₅ :
  HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) =
    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₆ : HMul.hMul (α := α) 1 (det.{u_4, u_3} (n := n) 1) *
      (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
    HMul.hMul (α := α) 1 (det.{u_4, u_3} (n := n) 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]
-- 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 α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
have haveI : ∀ (this : Invertible (α := Matrix m m α) 1), (fromBlocks 1 B C D).det = (D - C * B).det
Tactic: haveI : Invertible (1 : Matrix m m α) := invertibleOne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible (α := Matrix m m α) 1
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
have rw : det.{u_4, u_2} (n := m) 1 * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 1 _ * B).det =
  (D - C * B).det
Tactic: rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
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
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
have rw₁ : det.{u_4, u_2} (n := m) 1 * (D - C * 1 * B).det = (D - C * B).det
Tactic: rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
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
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
have rw₂ : det.{u_4, u_2} (n := m) 1 * (D - C * B).det = (D - C * B).det
Tactic: rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
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
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
have rw₃ : 1 * (D - C * B).det = (D - C * B).det
Tactic: rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
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
⊢ (fromBlocks 1 B C D).det = (D - C * B).det
have rw₄ : (D - C * B).det = (D - C * B).det
Tactic: rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
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)
have 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
Tactic: ext (i j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
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
have 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
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
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
⊢ 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
have 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
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
j : m ⊕ n
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
have 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)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
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)
⊢ 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
have 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)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
j : m ⊕ n
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
have 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)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
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)
⊢ 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
have 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)
Tactic: cases j
Cleared hypotheses: j
-- 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 α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible D
⊢ (fromBlocks A B C D).det = D.det * (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C).det
have 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)
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