[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
⊢ ∀ (e g : X ≃ᵈ Y),
    (fun f => ↑f.toEquiv) e = (fun f => ↑f.toEquiv) g → (fun f => ↑f.symm) e = (fun f => ↑f.symm) g → e = g
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h -
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝¹ x) (Equiv.toFun toEquiv✝¹ y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝ x) (Equiv.toFun toEquiv✝ y) = ↑r * edist x y
h :
  (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } =
    (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
⊢ { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } = { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝¹ x) (Equiv.toFun toEquiv✝¹ y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝ x) (Equiv.toFun toEquiv✝ y) = ↑r * edist x y
h :
  (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } =
    (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : Y), edist (Equiv.toFun e.symm x) (Equiv.toFun e.symm y) = ↑r * edist x y
[PROOFSTEP]
refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist (Equiv.toFun e.symm (↑e.toEquiv x)) (Equiv.toFun e.symm (↑e.toEquiv y)) =
    ↑(ratio e)⁻¹ * edist (↑e.toEquiv x) (↑e.toEquiv y)
[PROOFSTEP]
simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist x y = ↑(ratio e)⁻¹ * (↑(ratio e) * edist x y)
[PROOFSTEP]
rw [← mul_assoc, ← ENNReal.coe_mul, inv_mul_cancel (ratio_ne_zero e), ENNReal.coe_one, one_mul]
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : PseudoEMetricSpace X✝
inst✝² : PseudoEMetricSpace Y
inst✝¹ : PseudoEMetricSpace Z
X : Type u_4
inst✝ : PseudoEMetricSpace X
x✝¹ x✝ : X
⊢ edist (Equiv.toFun (Equiv.refl X) x✝¹) (Equiv.toFun (Equiv.refl X) x✝) = ↑1 * edist x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
by_cases hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
have hY : ∀ x y : Y, edist x y = 0 ∨ edist x y = ∞ :=
  e.surjective.forall₂.2 fun x y ↦ by refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
x y : X
⊢ edist (↑e x) (↑e y) = 0 ∨ edist (↑e x) (↑e y) = ⊤
[PROOFSTEP]
refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_
[GOAL]
case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
x y : X
h : edist x y = 0
⊢ edist (↑e x) (↑e y) = 0
[PROOFSTEP]
simp [*, Dilation.ratio_ne_zero]
[GOAL]
case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
x y : X
h : edist x y = ⊤
⊢ edist (↑e x) (↑e y) = ⊤
[PROOFSTEP]
simp [*, Dilation.ratio_ne_zero]
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
hY : ∀ (x y : Y), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
simp [Dilation.ratio_of_trivial, *]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ¬∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
push_neg at hX
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
exact (Dilation.ratio_comp' (g := e'.toDilation) (f := e.toDilation) hX).trans (mul_comm _ _)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
⊢ ratio (symm e) * ratio e = 1
[PROOFSTEP]
rw [← ratio_trans, symm_trans_self, ratio_refl]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ X
n : ℕ
⊢ ↑(e ^ n) = (↑e)^[n]
[PROOFSTEP]
rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ X
n : ℕ
⊢ (↑(↑toPerm e))^[n] = (↑e)^[n]
[PROOFSTEP]
rfl


[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix l m α
D : Matrix l n α
inst✝ : Invertible A
⊢ fromBlocks A B C D = fromBlocks 1 0 (C * ⅟A) 1 * fromBlocks A 0 0 (D - C * ⅟A * B) * fromBlocks 1 (⅟A * B) 0 1
[PROOFSTEP]
simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add, Matrix.one_mul, Matrix.mul_one,
  invOf_mul_self, Matrix.mul_invOf_self_assoc, Matrix.mul_invOf_mul_self_cancel, Matrix.mul_assoc,
  add_sub_cancel'_right]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix l m α
B : Matrix l n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ ↑(reindex (Equiv.sumComm l n) (Equiv.sumComm m n)) (fromBlocks A B C D) =
    ↑(reindex (Equiv.sumComm l n) (Equiv.sumComm m n))
      (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
[PROOFSTEP]
simpa [reindex_apply, Equiv.sumComm_symm, ← submatrix_mul_equiv _ _ _ (Equiv.sumComm n m), ←
  submatrix_mul_equiv _ _ _ (Equiv.sumComm n l), Equiv.sumComm_apply, fromBlocks_submatrix_sum_swap_sum_swap] using
  fromBlocks_eq_of_invertible₁₁ D C B A
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D * fromBlocks A B 0 D = 1
[PROOFSTEP]
simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero, Matrix.neg_mul, invOf_mul_self,
  Matrix.mul_invOf_mul_self_cancel, add_right_neg, fromBlocks_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D * fromBlocks A 0 C D = 1
[PROOFSTEP]
simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero, Matrix.neg_mul, invOf_mul_self,
  Matrix.mul_invOf_mul_self_cancel, add_left_neg, fromBlocks_one]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D
[PROOFSTEP]
letI := fromBlocksZero₂₁Invertible A B D
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
this : Invertible (fromBlocks A B 0 D) := fromBlocksZero₂₁Invertible A B D
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D
[PROOFSTEP]
convert (rfl : ⅟(fromBlocks A B 0 D) = _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A 0 C D)
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D
[PROOFSTEP]
letI := fromBlocksZero₁₂Invertible A C D
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A 0 C D)
this : Invertible (fromBlocks A 0 C D) := fromBlocksZero₁₂Invertible A C D
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D
[PROOFSTEP]
convert (rfl : ⅟(fromBlocks A 0 C D) = _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
⊢ toBlocks₁₁ ⅟(fromBlocks A B 0 D) * A = 1
[PROOFSTEP]
have := invOf_mul_self (fromBlocks A B 0 D)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this : ⅟(fromBlocks A B 0 D) * fromBlocks A B 0 D = 1
⊢ toBlocks₁₁ ⅟(fromBlocks A B 0 D) * A = 1
[PROOFSTEP]
rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks (toBlocks₁₁ ⅟(fromBlocks A B 0 D) * A + toBlocks₁₂ ⅟(fromBlocks A B 0 D) * 0)
      (toBlocks₁₁ ⅟(fromBlocks A B 0 D) * B + toBlocks₁₂ ⅟(fromBlocks A B 0 D) * D)
      (toBlocks₂₁ ⅟(fromBlocks A B 0 D) * A + toBlocks₂₂ ⅟(fromBlocks A B 0 D) * 0)
      (toBlocks₂₁ ⅟(fromBlocks A B 0 D) * B + toBlocks₂₂ ⅟(fromBlocks A B 0 D) * D) =
    1
⊢ toBlocks₁₁ ⅟(fromBlocks A B 0 D) * A = 1
[PROOFSTEP]
replace := congr_arg Matrix.toBlocks₁₁ this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  toBlocks₁₁
      (fromBlocks (toBlocks₁₁ ⅟(fromBlocks A B 0 D) * A + toBlocks₁₂ ⅟(fromBlocks A B 0 D) * 0)
        (toBlocks₁₁ ⅟(fromBlocks A B 0 D) * B + toBlocks₁₂ ⅟(fromBlocks A B 0 D) * D)
        (toBlocks₂₁ ⅟(fromBlocks A B 0 D) * A + toBlocks₂₂ ⅟(fromBlocks A B 0 D) * 0)
        (toBlocks₂₁ ⅟(fromBlocks A B 0 D) * B + toBlocks₂₂ ⅟(fromBlocks A B 0 D) * D)) =
    toBlocks₁₁ 1
⊢ toBlocks₁₁ ⅟(fromBlocks A B 0 D) * A = 1
[PROOFSTEP]
simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.mul_zero, add_zero, ← fromBlocks_one] using this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
⊢ D * toBlocks₂₂ ⅟(fromBlocks A B 0 D) = 1
[PROOFSTEP]
have := mul_invOf_self (fromBlocks A B 0 D)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this : fromBlocks A B 0 D * ⅟(fromBlocks A B 0 D) = 1
⊢ D * toBlocks₂₂ ⅟(fromBlocks A B 0 D) = 1
[PROOFSTEP]
rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks (A * toBlocks₁₁ ⅟(fromBlocks A B 0 D) + B * toBlocks₂₁ ⅟(fromBlocks A B 0 D))
      (A * toBlocks₁₂ ⅟(fromBlocks A B 0 D) + B * toBlocks₂₂ ⅟(fromBlocks A B 0 D))
      (0 * toBlocks₁₁ ⅟(fromBlocks A B 0 D) + D * toBlocks₂₁ ⅟(fromBlocks A B 0 D))
      (0 * toBlocks₁₂ ⅟(fromBlocks A B 0 D) + D * toBlocks₂₂ ⅟(fromBlocks A B 0 D)) =
    1
⊢ D * toBlocks₂₂ ⅟(fromBlocks A B 0 D) = 1
[PROOFSTEP]
replace := congr_arg Matrix.toBlocks₂₂ this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  toBlocks₂₂
      (fromBlocks (A * toBlocks₁₁ ⅟(fromBlocks A B 0 D) + B * toBlocks₂₁ ⅟(fromBlocks A B 0 D))
        (A * toBlocks₁₂ ⅟(fromBlocks A B 0 D) + B * toBlocks₂₂ ⅟(fromBlocks A B 0 D))
        (0 * toBlocks₁₁ ⅟(fromBlocks A B 0 D) + D * toBlocks₂₁ ⅟(fromBlocks A B 0 D))
        (0 * toBlocks₁₂ ⅟(fromBlocks A B 0 D) + D * toBlocks₂₂ ⅟(fromBlocks A B 0 D))) =
    toBlocks₂₂ 1
⊢ D * toBlocks₂₂ ⅟(fromBlocks A B 0 D) = 1
[PROOFSTEP]
simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.zero_mul, zero_add, ← fromBlocks_one] using this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
⊢ A * toBlocks₁₁ ⅟(fromBlocks A 0 C D) = 1
[PROOFSTEP]
have := mul_invOf_self (fromBlocks A 0 C D)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this : fromBlocks A 0 C D * ⅟(fromBlocks A 0 C D) = 1
⊢ A * toBlocks₁₁ ⅟(fromBlocks A 0 C D) = 1
[PROOFSTEP]
rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks (A * toBlocks₁₁ ⅟(fromBlocks A 0 C D) + 0 * toBlocks₂₁ ⅟(fromBlocks A 0 C D))
      (A * toBlocks₁₂ ⅟(fromBlocks A 0 C D) + 0 * toBlocks₂₂ ⅟(fromBlocks A 0 C D))
      (C * toBlocks₁₁ ⅟(fromBlocks A 0 C D) + D * toBlocks₂₁ ⅟(fromBlocks A 0 C D))
      (C * toBlocks₁₂ ⅟(fromBlocks A 0 C D) + D * toBlocks₂₂ ⅟(fromBlocks A 0 C D)) =
    1
⊢ A * toBlocks₁₁ ⅟(fromBlocks A 0 C D) = 1
[PROOFSTEP]
replace := congr_arg Matrix.toBlocks₁₁ this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  toBlocks₁₁
      (fromBlocks (A * toBlocks₁₁ ⅟(fromBlocks A 0 C D) + 0 * toBlocks₂₁ ⅟(fromBlocks A 0 C D))
        (A * toBlocks₁₂ ⅟(fromBlocks A 0 C D) + 0 * toBlocks₂₂ ⅟(fromBlocks A 0 C D))
        (C * toBlocks₁₁ ⅟(fromBlocks A 0 C D) + D * toBlocks₂₁ ⅟(fromBlocks A 0 C D))
        (C * toBlocks₁₂ ⅟(fromBlocks A 0 C D) + D * toBlocks₂₂ ⅟(fromBlocks A 0 C D))) =
    toBlocks₁₁ 1
⊢ A * toBlocks₁₁ ⅟(fromBlocks A 0 C D) = 1
[PROOFSTEP]
simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.zero_mul, add_zero, ← fromBlocks_one] using this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
⊢ toBlocks₂₂ ⅟(fromBlocks A 0 C D) * D = 1
[PROOFSTEP]
have := invOf_mul_self (fromBlocks A 0 C D)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this : ⅟(fromBlocks A 0 C D) * fromBlocks A 0 C D = 1
⊢ toBlocks₂₂ ⅟(fromBlocks A 0 C D) * D = 1
[PROOFSTEP]
rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks (toBlocks₁₁ ⅟(fromBlocks A 0 C D) * A + toBlocks₁₂ ⅟(fromBlocks A 0 C D) * C)
      (toBlocks₁₁ ⅟(fromBlocks A 0 C D) * 0 + toBlocks₁₂ ⅟(fromBlocks A 0 C D) * D)
      (toBlocks₂₁ ⅟(fromBlocks A 0 C D) * A + toBlocks₂₂ ⅟(fromBlocks A 0 C D) * C)
      (toBlocks₂₁ ⅟(fromBlocks A 0 C D) * 0 + toBlocks₂₂ ⅟(fromBlocks A 0 C D) * D) =
    1
⊢ toBlocks₂₂ ⅟(fromBlocks A 0 C D) * D = 1
[PROOFSTEP]
replace := congr_arg Matrix.toBlocks₂₂ this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  toBlocks₂₂
      (fromBlocks (toBlocks₁₁ ⅟(fromBlocks A 0 C D) * A + toBlocks₁₂ ⅟(fromBlocks A 0 C D) * C)
        (toBlocks₁₁ ⅟(fromBlocks A 0 C D) * 0 + toBlocks₁₂ ⅟(fromBlocks A 0 C D) * D)
        (toBlocks₂₁ ⅟(fromBlocks A 0 C D) * A + toBlocks₂₂ ⅟(fromBlocks A 0 C D) * C)
        (toBlocks₂₁ ⅟(fromBlocks A 0 C D) * 0 + toBlocks₂₂ ⅟(fromBlocks A 0 C D) * D)) =
    toBlocks₂₂ 1
⊢ toBlocks₂₂ ⅟(fromBlocks A 0 C D) * D = 1
[PROOFSTEP]
simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.mul_zero, zero_add, ← fromBlocks_one] using this
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
i : Invertible A × Invertible D
⊢ Invertible (fromBlocks A B 0 D)
[PROOFSTEP]
letI := i.1
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
i : Invertible A × Invertible D
this : Invertible A := i.fst
⊢ Invertible (fromBlocks A B 0 D)
[PROOFSTEP]
letI := i.2
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
i : Invertible A × Invertible D
this✝ : Invertible A := i.fst
this : Invertible D := i.snd
⊢ Invertible (fromBlocks A B 0 D)
[PROOFSTEP]
exact fromBlocksZero₂₁Invertible A B D
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
i : Invertible A × Invertible D
⊢ Invertible (fromBlocks A 0 C D)
[PROOFSTEP]
letI := i.1
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
i : Invertible A × Invertible D
this : Invertible A := i.fst
⊢ Invertible (fromBlocks A 0 C D)
[PROOFSTEP]
letI := i.2
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
i : Invertible A × Invertible D
this✝ : Invertible A := i.fst
this : Invertible D := i.snd
⊢ Invertible (fromBlocks A 0 C D)
[PROOFSTEP]
exact fromBlocksZero₁₂Invertible A C D
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
⊢ IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod, (fromBlocksZero₂₁InvertibleEquiv _ _ _).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
⊢ IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod, (fromBlocksZero₁₂InvertibleEquiv _ _ _).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
by_cases hA : IsUnit A
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
have hD := hAD.mp hA
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
cases hA.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
cases hD.nonempty_invertible
[GOAL]
case pos.intro.intro
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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✝ : Invertible D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
[PROOFSTEP]
letI := fromBlocksZero₂₁Invertible A B D
[GOAL]
case pos.intro.intro
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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✝ : Invertible D
this : Invertible (fromBlocks A B 0 D) := fromBlocksZero₂₁Invertible A B D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
[PROOFSTEP]
simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₂₁_eq]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
have hD := hAD.not.mp hA
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
have : ¬IsUnit (fromBlocks A B 0 D) := isUnit_fromBlocks_zero₂₁.not.mpr (not_and'.mpr fun _ => hA)
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
  Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
by_cases hA : IsUnit A
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
have hD := hAD.mp hA
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
cases hA.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
cases hD.nonempty_invertible
[GOAL]
case pos.intro.intro
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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✝ : Invertible D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
[PROOFSTEP]
letI := fromBlocksZero₁₂Invertible A C D
[GOAL]
case pos.intro.intro
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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✝ : Invertible D
this : Invertible (fromBlocks A 0 C D) := fromBlocksZero₁₂Invertible A C D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
[PROOFSTEP]
simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₁₂_eq]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
have hD := hAD.not.mp hA
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
have : ¬IsUnit (fromBlocks A 0 C D) := isUnit_fromBlocks_zero₁₂.not.mpr (not_and'.mpr fun _ => hA)
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : 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⁻¹
[PROOFSTEP]
simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
  Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible (fromBlocks A B C D)
[PROOFSTEP]
refine'
  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₂₂ _ _ _ _) _
[GOAL]
case refine'_1
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
[PROOFSTEP]
letI : Invertible (1 : Matrix n n α) := invertibleOne
[GOAL]
case refine'_1
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
[PROOFSTEP]
letI : Invertible (1 : Matrix m m α) := invertibleOne
[GOAL]
case refine'_1
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
[PROOFSTEP]
refine' Invertible.mul _ (fromBlocksZero₁₂Invertible _ _ _)
[GOAL]
case refine'_1
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
exact Invertible.mul (fromBlocksZero₂₁Invertible _ _ _) (fromBlocksZero₂₁Invertible _ _ _)
[GOAL]
case refine'_2
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ 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 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
[PROOFSTEP]
show
  _ =
    fromBlocks 1 0 (-(1 * (⅟D * C) * 1)) 1 *
      (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * 0 * ⅟D)) 0 (⅟D) * fromBlocks 1 (-(1 * (B * ⅟D) * 1)) 0 1)
        -- combine into a single block matrix
[GOAL]
case refine'_2
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ 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 1 0 (-(1 * (⅟D * C) * 1)) 1 *
      (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * 0 * ⅟D)) 0 ⅟D * fromBlocks 1 (-(1 * (B * ⅟D) * 1)) 0 1)
[PROOFSTEP]
simp only [fromBlocks_multiply, invOf_one, Matrix.one_mul, Matrix.mul_one, Matrix.zero_mul, Matrix.mul_zero, add_zero,
  zero_add, neg_zero, Matrix.mul_neg, Matrix.neg_mul, neg_neg, ← Matrix.mul_assoc, add_comm (⅟D)]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (D - C * ⅟A * B)
⊢ Invertible (fromBlocks A B C D)
[PROOFSTEP]
letI := fromBlocks₂₂Invertible D C B A
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (D - C * ⅟A * B)
this : Invertible (fromBlocks D C B A) := fromBlocks₂₂Invertible D C B A
⊢ Invertible (fromBlocks A B C D)
[PROOFSTEP]
letI iDCBA := submatrixEquivInvertible (fromBlocks D C B A) (Equiv.sumComm _ _) (Equiv.sumComm _ _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (D - C * ⅟A * B)
this : Invertible (fromBlocks D C B A) := fromBlocks₂₂Invertible D C B A
iDCBA : Invertible (submatrix (fromBlocks D C B A) ↑(Equiv.sumComm m n) ↑(Equiv.sumComm m n)) :=
  submatrixEquivInvertible (fromBlocks D C B A) (Equiv.sumComm m n) (Equiv.sumComm m n)
⊢ Invertible (fromBlocks A B C D)
[PROOFSTEP]
exact
  iDCBA.copy' _
    (fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) (⅟(D - C * ⅟A * B)))
    (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    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)
[PROOFSTEP]
letI := fromBlocks₂₂Invertible A B C D
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := fromBlocks₂₂Invertible A B C D
⊢ ⅟(fromBlocks A B C D) =
    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)
[PROOFSTEP]
convert (rfl : ⅟(fromBlocks A B C D) = _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible (D - C * ⅟A * B)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)
[PROOFSTEP]
letI := fromBlocks₁₁Invertible A B C D
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁹ : Fintype l
inst✝⁸ : Fintype m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible (D - C * ⅟A * B)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := fromBlocks₁₁Invertible A B C D
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)
[PROOFSTEP]
convert (rfl : ⅟(fromBlocks A B C D) = _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (A - B * ⅟D * C)
[PROOFSTEP]
suffices Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D) by
  exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
⊢ Invertible (A - B * ⅟D * C)
[PROOFSTEP]
exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
letI : Invertible (1 : Matrix n n α) := invertibleOne
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
letI : Invertible (1 : Matrix m m α) := invertibleOne
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
letI iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1 : Matrix (Sum m n) (Sum m n) α) := fromBlocksZero₁₂Invertible _ _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1) := fromBlocksZero₁₂Invertible 1 (⅟D * C) 1
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
letI iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1 : Matrix (Sum m n) (Sum m n) α) := fromBlocksZero₂₁Invertible _ _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1) := fromBlocksZero₁₂Invertible 1 (⅟D * C) 1
iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1) := fromBlocksZero₂₁Invertible 1 (B * ⅟D) 1
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
letI iBDC := Invertible.copy ‹_› _ (fromBlocks_eq_of_invertible₂₂ A B C D).symm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1) := fromBlocksZero₁₂Invertible 1 (⅟D * C) 1
iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1) := fromBlocksZero₂₁Invertible 1 (B * ⅟D) 1
iBDC : Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1) :=
  Invertible.copy inst✝ (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
    (_ : fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1 = fromBlocks A B C D)
⊢ Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
refine' (iBD.mulLeft _).symm _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this✝ : Invertible 1 := invertibleOne
this : Invertible 1 := invertibleOne
iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1) := fromBlocksZero₁₂Invertible 1 (⅟D * C) 1
iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1) := fromBlocksZero₂₁Invertible 1 (B * ⅟D) 1
iBDC : Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1) :=
  Invertible.copy inst✝ (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
    (_ : fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1 = fromBlocks A B C D)
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D)
[PROOFSTEP]
refine' (iDC.mulRight _).symm iBDC
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (D - C * ⅟A * B)
[PROOFSTEP]
letI iABCD' := submatrixEquivInvertible (fromBlocks A B C D) (Equiv.sumComm _ _) (Equiv.sumComm _ _)
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (fromBlocks A B C D)
iABCD' : Invertible (submatrix (fromBlocks A B C D) ↑(Equiv.sumComm n m) ↑(Equiv.sumComm n m)) :=
  submatrixEquivInvertible (fromBlocks A B C D) (Equiv.sumComm n m) (Equiv.sumComm n m)
⊢ Invertible (D - C * ⅟A * B)
[PROOFSTEP]
letI iDCBA := iABCD'.copy _ (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (fromBlocks A B C D)
iABCD' : Invertible (submatrix (fromBlocks A B C D) ↑(Equiv.sumComm n m) ↑(Equiv.sumComm n m)) :=
  submatrixEquivInvertible (fromBlocks A B C D) (Equiv.sumComm n m) (Equiv.sumComm n m)
iDCBA : Invertible (fromBlocks D C B A) :=
  Invertible.copy iABCD' (fromBlocks D C B A)
    (_ : fromBlocks D C B A = submatrix (fromBlocks A B C D) Sum.swap Sum.swap)
⊢ Invertible (D - C * ⅟A * B)
[PROOFSTEP]
refine' invertibleOfFromBlocks₂₂Invertible D C B A
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivFromBlocks₂₂Invertible A B C D).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivFromBlocks₁₁Invertible A B C D).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ det (fromBlocks A B C D) = det A * det (D - C * ⅟A * B)
[PROOFSTEP]
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]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ det (fromBlocks 1 B C D) = det (D - C * B)
[PROOFSTEP]
haveI : Invertible (1 : Matrix m m α) := invertibleOne
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
this : Invertible 1
⊢ det (fromBlocks 1 B C D) = det (D - C * B)
[PROOFSTEP]
rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ det (fromBlocks A B C D) = det D * det (A - B * ⅟D * C)
[PROOFSTEP]
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
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ fromBlocks A B C D = submatrix (fromBlocks D C B A) ↑(Equiv.sumComm m n) ↑(Equiv.sumComm m n)
[PROOFSTEP]
ext (i j)
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
i j : m ⊕ n
⊢ fromBlocks A B C D i j = submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) i j
[PROOFSTEP]
cases i
[GOAL]
case a.h.inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
j : m ⊕ n
val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝) j =
    submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) (Sum.inl val✝) j
[PROOFSTEP]
cases j
[GOAL]
case a.h.inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
j : m ⊕ n
val✝ : n
⊢ fromBlocks A B C D (Sum.inr val✝) j =
    submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) (Sum.inr val✝) j
[PROOFSTEP]
cases j
[GOAL]
case a.h.inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) =
    submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) =
    submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) =
    submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : n
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) =
    submatrix (fromBlocks D C B A) (↑(Equiv.sumComm m n)) (↑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
this : fromBlocks A B C D = submatrix (fromBlocks D C B A) ↑(Equiv.sumComm m n) ↑(Equiv.sumComm m n)
⊢ det (fromBlocks A B C D) = det D * det (A - B * ⅟D * C)
[PROOFSTEP]
rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
⊢ det (fromBlocks A B C 1) = det (A - B * C)
[PROOFSTEP]
haveI : Invertible (1 : Matrix n n α) := invertibleOne
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ det (fromBlocks A B C 1) = det (A - B * C)
[PROOFSTEP]
rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ det (1 + A * B) = det (fromBlocks 1 (-A) B 1)
[PROOFSTEP]
rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ det (fromBlocks 1 (-A) B 1) = det (1 + B * A)
[PROOFSTEP]
rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ det (A * B + 1) = det (B * A + 1)
[PROOFSTEP]
rw [add_comm, det_one_add_mul_comm, add_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ det (1 - A * B) = det (1 - B * A)
[PROOFSTEP]
rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁶ : Fintype l
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
u v : m → α
⊢ det (1 + col u * row v) = 1 + v ⬝ᵥ u
[PROOFSTEP]
rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq, Matrix.row_mul_col_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : IsHermitian A
⊢ vecMul (star (x ⊕ᵥ y)) (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
    vecMul (star (x + mulVec (A⁻¹ * B) y)) A ⬝ᵥ (x + mulVec (A⁻¹ * B) y) + vecMul (star y) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y
[PROOFSTEP]
simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul, dotProduct_mulVec, vecMul_sub,
  Matrix.mul_assoc, vecMul_mulVec, hA.eq, conjTranspose_nonsing_inv, star_mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : IsHermitian A
⊢ vecMul (star x) A ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x + (vecMul (star x) B ⬝ᵥ y + vecMul (star y) D ⬝ᵥ y) =
    vecMul (star x) A ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x +
        (vecMul (star x) B ⬝ᵥ y + vecMul (star y) (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (vecMul (star y) D ⬝ᵥ y - vecMul (star y) (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)
[PROOFSTEP]
abel
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : IsHermitian A
⊢ vecMul (star x) A ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x + (vecMul (star x) B ⬝ᵥ y + vecMul (star y) D ⬝ᵥ y) =
    vecMul (star x) A ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x +
        (vecMul (star x) B ⬝ᵥ y + vecMul (star y) (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (vecMul (star y) D ⬝ᵥ y - vecMul (star y) (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)
[PROOFSTEP]
abel
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : IsHermitian D
⊢ vecMul (star (x ⊕ᵥ y)) (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
    vecMul (star (mulVec (D⁻¹ * Bᴴ) x + y)) D ⬝ᵥ (mulVec (D⁻¹ * Bᴴ) x + y) + vecMul (star x) (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x
[PROOFSTEP]
simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul, dotProduct_mulVec, vecMul_sub,
  Matrix.mul_assoc, vecMul_mulVec, hD.eq, conjTranspose_nonsing_inv, star_mulVec]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : IsHermitian D
⊢ vecMul (star x) A ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x + (vecMul (star x) B ⬝ᵥ y + vecMul (star y) D ⬝ᵥ y) =
    vecMul (star x) (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x +
        (vecMul (star x) B ⬝ᵥ y + vecMul (star y) D ⬝ᵥ y) +
      (vecMul (star x) A ⬝ᵥ x - vecMul (star x) (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)
[PROOFSTEP]
abel
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : IsHermitian D
⊢ vecMul (star x) A ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x + (vecMul (star x) B ⬝ᵥ y + vecMul (star y) D ⬝ᵥ y) =
    vecMul (star x) (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + vecMul (star y) Bᴴ ⬝ᵥ x +
        (vecMul (star x) B ⬝ᵥ y + vecMul (star y) D ⬝ᵥ y) +
      (vecMul (star x) A ⬝ᵥ x - vecMul (star x) (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)
[PROOFSTEP]
abel
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
⊢ IsHermitian (Matrix.fromBlocks A B Bᴴ D) ↔ IsHermitian (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian :=
  by
  apply isHermitian_conjTranspose_mul_mul
  apply hA.inv
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
⊢ IsHermitian (Bᴴ * A⁻¹ * B)
[PROOFSTEP]
apply isHermitian_conjTranspose_mul_mul
[GOAL]
case hA
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
⊢ IsHermitian A⁻¹
[PROOFSTEP]
apply hA.inv
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
⊢ IsHermitian (Matrix.fromBlocks A B Bᴴ D) ↔ IsHermitian (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
rw [isHermitian_fromBlocks_iff]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
⊢ IsHermitian A ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ IsHermitian D ↔ IsHermitian (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
constructor
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
⊢ IsHermitian A ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ IsHermitian D → IsHermitian (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
intro h
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
h : IsHermitian A ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ IsHermitian D
⊢ IsHermitian (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
apply IsHermitian.sub h.2.2.2 hBAB
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
⊢ IsHermitian (D - Bᴴ * A⁻¹ * B) → IsHermitian A ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ IsHermitian D
[PROOFSTEP]
intro h
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
h : IsHermitian (D - Bᴴ * A⁻¹ * B)
⊢ IsHermitian A ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ IsHermitian D
[PROOFSTEP]
refine' ⟨hA, rfl, conjTranspose_conjTranspose B, _⟩
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
h : IsHermitian (D - Bᴴ * A⁻¹ * B)
⊢ IsHermitian D
[PROOFSTEP]
rw [← sub_add_cancel D]
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
h : IsHermitian (D - Bᴴ * A⁻¹ * B)
⊢ IsHermitian (D - ?mpr + ?mpr)
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : IsHermitian A
hBAB : IsHermitian (Bᴴ * A⁻¹ * B)
h : IsHermitian (D - Bᴴ * A⁻¹ * B)
⊢ Matrix n n 𝕜
[PROOFSTEP]
apply IsHermitian.add h hBAB
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : IsHermitian D
⊢ IsHermitian (Matrix.fromBlocks A B Bᴴ D) ↔ IsHermitian (A - B * D⁻¹ * Bᴴ)
[PROOFSTEP]
rw [← isHermitian_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply, fromBlocks_submatrix_sum_swap_sum_swap]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : IsHermitian D
⊢ IsHermitian (Matrix.fromBlocks D Bᴴ B A) ↔ IsHermitian (A - B * D⁻¹ * Bᴴ)
[PROOFSTEP]
convert IsHermitian.fromBlocks₁₁ _ _ hD
[GOAL]
case h.e'_1.h.e'_4.h.e'_8
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : IsHermitian D
⊢ B = Bᴴᴴ
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_4.h.e'_6.h.e'_5.h.e'_5
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : IsHermitian D
⊢ B = Bᴴᴴ
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
⊢ PosSemidef (fromBlocks A B Bᴴ D) ↔ PosSemidef (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
rw [PosSemidef, IsHermitian.fromBlocks₁₁ _ _ hA.1]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
⊢ (IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x) ↔
    PosSemidef (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
constructor
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
⊢ (IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x) →
    PosSemidef (D - Bᴴ * A⁻¹ * B)
[PROOFSTEP]
refine' fun h => ⟨h.1, fun x => _⟩
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ mulVec (D - Bᴴ * A⁻¹ * B) x
[PROOFSTEP]
have := h.2 (-(A⁻¹ * B).mulVec x ⊕ᵥ x)
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x
x : n → 𝕜
this : 0 ≤ star (-mulVec (A⁻¹ * B) x ⊕ᵥ x) ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) (-mulVec (A⁻¹ * B) x ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ mulVec (D - Bᴴ * A⁻¹ * B) x
[PROOFSTEP]
rw [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_self, dotProduct_zero, zero_add] at this
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x
x : n → 𝕜
this : 0 ≤ vecMul (star x) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ⬝ᵥ mulVec (D - Bᴴ * A⁻¹ * B) x
[PROOFSTEP]
rw [dotProduct_mulVec]
[GOAL]
case mp
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x
x : n → 𝕜
this : 0 ≤ vecMul (star x) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ vecMul (star x) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
[PROOFSTEP]
exact this
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
⊢ PosSemidef (D - Bᴴ * A⁻¹ * B) →
    IsHermitian (D - Bᴴ * A⁻¹ * B) ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x
[PROOFSTEP]
refine' fun h => ⟨h.1, fun x => _⟩
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : PosSemidef (D - Bᴴ * A⁻¹ * B)
x : m ⊕ n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ mulVec (fromBlocks A B Bᴴ D) x
[PROOFSTEP]
rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]
[GOAL]
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : PosSemidef (D - Bᴴ * A⁻¹ * B)
x : m ⊕ n → 𝕜
⊢ 0 ≤
    vecMul (star (x ∘ Sum.inl + mulVec (A⁻¹ * B) (x ∘ Sum.inr))) A ⬝ᵥ (x ∘ Sum.inl + mulVec (A⁻¹ * B) (x ∘ Sum.inr)) +
      vecMul (star (x ∘ Sum.inr)) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
[PROOFSTEP]
apply le_add_of_nonneg_of_le
[GOAL]
case mpr.ha
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : PosSemidef (D - Bᴴ * A⁻¹ * B)
x : m ⊕ n → 𝕜
⊢ 0 ≤ vecMul (star (x ∘ Sum.inl + mulVec (A⁻¹ * B) (x ∘ Sum.inr))) A ⬝ᵥ (x ∘ Sum.inl + mulVec (A⁻¹ * B) (x ∘ Sum.inr))
[PROOFSTEP]
rw [← dotProduct_mulVec]
[GOAL]
case mpr.ha
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : PosSemidef (D - Bᴴ * A⁻¹ * B)
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inl + mulVec (A⁻¹ * B) (x ∘ Sum.inr)) ⬝ᵥ mulVec A (x ∘ Sum.inl + mulVec (A⁻¹ * B) (x ∘ Sum.inr))
[PROOFSTEP]
apply hA.posSemidef.2
[GOAL]
case mpr.hbc
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : PosSemidef (D - Bᴴ * A⁻¹ * B)
x : m ⊕ n → 𝕜
⊢ 0 ≤ vecMul (star (x ∘ Sum.inr)) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
[PROOFSTEP]
rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]
[GOAL]
case mpr.hbc
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hA : PosDef A
inst✝ : Invertible A
h : PosSemidef (D - Bᴴ * A⁻¹ * B)
x : m ⊕ n → 𝕜
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ mulVec (D - Bᴴ * A⁻¹ * B) (x ∘ Sum.inr)
[PROOFSTEP]
apply h.2
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ PosSemidef (fromBlocks A B Bᴴ D) ↔ PosSemidef (A - B * D⁻¹ * Bᴴ)
[PROOFSTEP]
rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply, fromBlocks_submatrix_sum_swap_sum_swap]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ PosSemidef (fromBlocks D Bᴴ B A) ↔ PosSemidef (A - B * D⁻¹ * Bᴴ)
[PROOFSTEP]
convert PosSemidef.fromBlocks₁₁ Bᴴ A hD
[GOAL]
case h.e'_1.h.e'_7.h.e'_8
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ B = Bᴴᴴ
[PROOFSTEP]
first
| infer_instance
| simp
[GOAL]
case h.e'_1.h.e'_7.h.e'_8
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ B = Bᴴᴴ
[PROOFSTEP]
infer_instance
[GOAL]
case h.e'_1.h.e'_7.h.e'_8
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ B = Bᴴᴴ
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_7.h.e'_6.h.e'_5.h.e'_5
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ B = Bᴴᴴ
[PROOFSTEP]
first
| infer_instance
| simp
[GOAL]
case h.e'_2.h.e'_7.h.e'_6.h.e'_5.h.e'_5
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ B = Bᴴᴴ
[PROOFSTEP]
infer_instance
[GOAL]
case h.e'_2.h.e'_7.h.e'_6.h.e'_5.h.e'_5
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : StarOrderedRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : PosDef D
inst✝ : Invertible D
⊢ B = Bᴴᴴ
[PROOFSTEP]
simp