-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_inv_of_blockTriangular [LinearOrder α] [Invertible M]
    (hM : BlockTriangular M b) : BlockTriangular M⁻¹ b

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
suffices ∀ hs : Finset α, univ.image b = hs → BlockTriangular M⁻¹ b by exact this _ rfl

Result:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
⊢ ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b

Proof state:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
intro i j hij

Result:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
⊢ M⁻¹ i j = 0

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
exact this _ rfl

Result:
no goals

Proof state:
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
hb' : image b' univ ⊂ image b univ
⊢ b' ⟨j, ⋯⟩ < b' ⟨i, hi⟩

Tactic:
simp_rw [b', hij]

Result:
no goals

Proof state:
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
⊢ k ∈ image b univ

Tactic:
convert max'_mem (α := α) _ _

Result:
no goals

Proof state:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
⊢ M⁻¹ i j = 0

Tactic:
let b' := fun i : { a // b a < k } => b ↑i

Result:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
⊢ M⁻¹ i j = 0

Proof state:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
⊢ M⁻¹ i j = 0

Tactic:
let k := (univ.image b).max' (univ_nonempty.image _)

Result:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
⊢ M⁻¹ i j = 0

Proof state:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k
hi : b i < (image b univ).max' ⋯
⊢ M⁻¹ i j = 0

Tactic:
haveI : Invertible A := hM.invertibleToBlock _

Result:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
⊢ M⁻¹ i j = 0