Theorem: MatrixCookbook.eq_399 (MatrixCookbook/9SpecialMatrices.lean)

State before:
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₁ := A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁;
    let i := inst✝;
    (⅟C₁).fromBlocks (-(⅟C₁ * A₁₂ * ⅟A₂₂)) (-(⅟A₂₂ * A₂₁ * ⅟C₁)) (⅟A₂₂ + ⅟A₂₂ * A₂₁ * ⅟C₁ * A₁₂ * ⅟A₂₂)
Tactic:
letI := fromBlocks₂₂Invertible A₁₁ A₁₂ A₂₁ A₂₂
State after:
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₁ := A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁;
    let i := inst✝;
    (⅟C₁).fromBlocks (-(⅟C₁ * A₁₂ * ⅟A₂₂)) (-(⅟A₂₂ * A₂₁ * ⅟C₁)) (⅟A₂₂ + ⅟A₂₂ * A₂₁ * ⅟C₁ * A₁₂ * ⅟A₂₂)

State before:
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₁ := A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁;
    let i := inst✝;
    (⅟C₁).fromBlocks (-(⅟C₁ * A₁₂ * ⅟A₂₂)) (-(⅟A₂₂ * A₂₁ * ⅟C₁)) (⅟A₂₂ + ⅟A₂₂ * A₂₁ * ⅟C₁ * A₁₂ * ⅟A₂₂)
Tactic:
convert invOf_fromBlocks₂₂_eq A₁₁ A₁₂ A₂₁ A₂₂
State after:
case h.e'_2
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ = ⅟(A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)

State before:
case h.e'_2
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ = ⅟(A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)
Tactic:
rw [invOf_eq_nonsing_inv]
State after:
no goals