awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
D : Matrix n n α
inst_7 : Invertible A
inst_8 : Invertible D
simp_rw :
  fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * 0)
      (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₁ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + 0) (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
⊢ 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 =
    1
have simp_rw₂ : fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
      -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        D)
    (HAdd.hAdd (α := Matrix n m α) 0 0) (0 + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
  1
Tactic: simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
      fromBlocks_one]
-- 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 α
D : Matrix n n α
inst_7 : Invertible A
inst_8 : Invertible D
simp_rw :
  fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * 0)
      (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₁ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + 0) (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₂ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (HAdd.hAdd (α := Matrix n m α) 0 0) (0 + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
⊢ 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 =
    1
have simp_rw₃ : fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
      -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        D)
    0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
  1
Tactic: simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
      fromBlocks_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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) _).toBlocks₁₁ * A = 1
have this : @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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₁₁ * A = 1
have 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
Tactic: rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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)
⊢ D * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A B 0 D) _).toBlocks₂₂ = 1
have this : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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)
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ = 1
have this : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ = 1
have 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
Tactic: rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₁₁ = 1
have 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
Tactic: replace := congr_arg Matrix.toBlocks₁₁ this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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) _).toBlocks₂₂ * D = 1
have this : @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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D = 1
have 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
Tactic: rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (hypothesis)
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
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (fromBlocks A 0 C D) _).toBlocks₂₂ * D = 1
have 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
Tactic: replace := congr_arg Matrix.toBlocks₂₂ this
Cleared hypotheses: this
-- 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
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have pos : ∀ (hA : IsUnit A), (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 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 α
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⁻¹
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg : ∀ (hA : ¬IsUnit A), (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have pos : ∀ (val : Invertible A), (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val : Invertible A
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have pos : ∀ (val : Invertible D), (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 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 α
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
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have 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 _)
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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have this : ¬IsUnit (fromBlocks A B 0 D)
Tactic: have : ¬IsUnit (fromBlocks A B 0 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 α
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)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg : Ring.inverse (fromBlocks A B 0 D) =
  fromBlocks (Ring.inverse A) (-(Ring.inverse A * B * Ring.inverse D)) 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 α
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)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg₁ : Ring.inverse (fromBlocks A B 0 D) = fromBlocks 0 (-(0 * B * Ring.inverse D)) 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 α
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)
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
have neg₂ : Ring.inverse (fromBlocks A B 0 D) = 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]