case pos
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁

case neg
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
by_cases h : IsUnit A
case pos.intro
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
case pos
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
cases h.nonempty_invertible
case pos.intro
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
case pos.intro
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
letI := submatrixEquivInvertible A e₁ e₂
no goals
case pos.intro
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
case neg
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (submatrix A ↑e₁ ↑e₂)
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
case neg
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h
no goals
case neg
l : Type ?u.401048
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (submatrix A ↑e₁ ↑e₂)
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
  submatrix_zero, Pi.zero_apply]