awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq α
inst_4 : Fintype α
inst_5 : LinearOrder α
h : M.BlockTriangular b
a : α
h_1 : Membership.mem (γ := Finset α) univ a
ha : a ∉ image b univ
this : IsEmpty.{max 1 (u_3 + 1)} { i : m // b i = a }
⊢ (M.toSquareBlock b a).det = 1

Tactic:
exact det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
M : Matrix m m R
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder m
h : M.BlockTriangular id
haveI : ∀ (this : DecidableEq R), M.det = ∏ i : m, M i i
⊢ M.det = ∏ i : m, M i i

Tactic:
haveI : DecidableEq R := Classical.decEq _
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
M : Matrix m m R
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder m
h : M.BlockTriangular id
this : DecidableEq R
simp_rw : Eq.{v + 1} (α := R) (∏ a ∈ image id univ, (M.toSquareBlock id a).det) (∏ i : m, M i i)
simp_rw₁ : Eq.{v + 1} (α := R) (∏ x : m, (M.toSquareBlock id x).det) (∏ i : m, M i i)
⊢ M.det = ∏ i : m, M i i

Tactic:
simp_rw [h.det, image_id, det_toSquareBlock_id]

Premises used: Finset.image_id, Matrix.BlockTriangular.det, Matrix.det_toSquareBlock_id
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder m
M : Matrix m m R
h : M.BlockTriangular (α := mᵒᵈ) (⇑toDual : (a : m) → mᵒᵈ)
rw : Mᵀ.det = ∏ i : m, M i i
⊢ M.det = ∏ i : m, M i i

Tactic:
rw [← det_transpose]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder m
M : Matrix m m R
h : M.BlockTriangular (α := mᵒᵈ) (⇑toDual : (a : m) → mᵒᵈ)
⊢ Mᵀ.det = ∏ i : m, M i i

Tactic:
det_of_upperTriangular h.transpose

Premises used: Matrix.BlockTriangular.transpose, Matrix.transpose, Matrix.det_of_upperTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder m
M : Matrix m m R
h : M.BlockTriangular (α := mᵒᵈ) (⇑toDual : (a : m) → mᵒᵈ)
⊢ Mᵀ.det = ∏ i : m, M i i

Tactic:
exact det_of_upperTriangular h.transpose

Premises used: Matrix.BlockTriangular.transpose, Matrix.det_of_upperTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
R : Type u_9
inst : Semiring R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
x j : Fin n
h : id j < id x
⊢ Eq.{u_9 + 1} (α := R)
    ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)) x j : R)
    (0 : R)

Tactic:
coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h

Premises used: Nat.lt_of_le_of_lt, Polynomial.coeff, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
R : Type u_9
inst : Semiring R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
x j : Fin n
h : id j < id x
⊢ Eq.{u_9 + 1} (α := R)
    ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)) x j : R)
    (0 : R)

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h

Premises used: Nat.lt_of_le_of_lt, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
R : Type v
inst : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
rw :
  Eq.{v + 1} (α := R)
    (∏ i : Fin n,
      (of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)) i i)
    1
⊢ Eq.{v + 1} (α := R)
    (det (n := Fin n)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)))
    1

Tactic:
rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
      Nat.le_of_eq (h_deg i)))]

Premises used: Nat.le_of_eq, Matrix.matrixOfPolynomials_blockTriangular, Matrix.det_of_upperTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
R : Type v
inst : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ Eq.{v + 1} (α := R) (∏ _x : Fin n, 1) 1

Tactic:
prod_const_one

Premises used: Finset.prod_const_one
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
R : Type v
inst : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
h :
  ∀ (x : Fin n),
    Membership.mem (γ := Finset (Fin n)) univ x →
      Eq.{v + 1} (α := R)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)) x x : R)
        (1 : R)
⊢ Eq.{v + 1} (α := R)
    (∏ i : Fin n,
      (of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)) i i)
    1

Tactic:
convert! prod_const_one with x _

Premises used: Finset.prod_const_one
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
R : Type v
inst : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
x : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) univ x
h : (p x).coeff (↑x : ℕ) = 1
h₁ : (p x).coeff (p x).natDegree = 1
h₂ : (p x).leadingCoeff = 1
h₃ h₄ : Eq.{v + 1} (α := R) 1 1
⊢ Eq.{v + 1} (α := R)
    ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ)) x x : R)
    (1 : R)

Tactic:
rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]

Premises used: Polynomial.coeff_natDegree, Matrix.of_apply, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
rw : (M⁻¹ * M).toBlock p p = 1
rw₁ : Eq (α := Matrix.{u_3, u_3, v} { a : m // p a } { a : m // p a } R) (toBlock 1 p p) 1
rw₂ rw₃ : Eq (α := Matrix.{u_3, u_3, v} { a : m // p a } { a : m // p a } R) 1 1
⊢ M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun (i : m) ↦ ¬p i) * M.toBlock (fun (i : m) ↦ ¬p i) p = 1

Tactic:
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]

Premises used: Matrix.toBlock_mul_eq_add, Matrix.inv_mul_of_invertible, Matrix.toBlock_one_self
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
⊢ M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun (i : m) ↦ ¬p i) * M.toBlock (fun (i : m) ↦ ¬p i) p = 1

Tactic:
have h_sum :
    M⁻¹.toBlock p p * M.toBlock p p +
        (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p =
      1 := by
    rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun (i : m) ↦ ¬p i) * M.toBlock (fun (i : m) ↦ ¬p i) p = 1
a : ∀ (i : { a : m // ¬p a }) (j : { a : m // p a }), M.toBlock (fun (i : m) ↦ ¬p i) p i j = 0 i j
⊢ Eq (α := Matrix.{u_3, u_3, v} { a : m // ¬p a } { a : m // p a } R) (M.toBlock (fun (i : m) ↦ ¬p i) p) 0

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun (i : m) ↦ ¬p i) * M.toBlock (fun (i : m) ↦ ¬p i) p = 1
i : { a : m // ¬p a }
j : { a : m // p a }
⊢ M.toBlock (fun (i : m) ↦ ¬p i) p i j = 0 i j

Tactic:
simpa using hM (lt_of_lt_of_le j.2 (le_of_not_gt i.2))

Premises used: le_of_not_gt, lt_of_lt_of_le, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun (i : m) ↦ ¬p i) * M.toBlock (fun (i : m) ↦ ¬p i) p = 1
⊢ Eq (α := Matrix.{u_3, u_3, v} { a : m // ¬p a } { a : m // p a } R) (M.toBlock (fun (i : m) ↦ ¬p i) p) 0

Tactic:
have h_zero : M.toBlock (fun i => ¬p i) p = 0 := by
    ext i j
    simpa using hM (lt_of_lt_of_le j.2 (le_of_not_gt i.2))
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun (i : m) ↦ ¬p i) * M.toBlock (fun (i : m) ↦ ¬p i) p = 1
h_zero : Eq (α := Matrix.{u_3, u_3, v} { a : m // ¬p a } { a : m // p a } R) (M.toBlock (fun (i : m) ↦ ¬p i) p) 0
⊢ HMul.hMul (α := Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R)
      (M⁻¹.toBlock (fun (i : m) ↦ b i < k) fun (i : m) ↦ b i < k)
      (M.toBlock (fun (i : m) ↦ b i < k) fun (i : m) ↦ b i < k) =
    1

Tactic:
simpa [h_zero] using h_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
⊢ Eq (α := Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R)
    (M.toBlock (fun (i : m) ↦ b i < k) fun (i : m) ↦ b i < k)⁻¹
    (M⁻¹.toBlock (fun (i : m) ↦ b i < k) fun (i : m) ↦ b i < k)

Tactic:
inv_eq_left_inv <| hM.toBlock_inverse_mul_toBlock_eq_one k

Premises used: Matrix.inv_eq_left_inv, Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
A : Type u_8
M N : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : LinearOrder α
inst_6 : Invertible M
hM : M.BlockTriangular b
k : α
⊢ HMul.hMul (α := Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R)
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one M _).toBlock (fun (i : m) ↦ b i < k) fun (i : m) ↦
        b i < k)
      (M.toBlock (fun (i : m) ↦ b i < k) fun (i : m) ↦ b i < k) =
    1

Tactic:
simpa only [invOf_eq_nonsing_inv] using hM.toBlock_inverse_mul_toBlock_eq_one k

Premises used: Matrix.invOf_eq_nonsing_inv, Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
rw : Disjoint q p
⊢ M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0

Tactic:
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]

Premises used: Matrix.toBlock_one_disjoint, Matrix.toBlock_mul_eq_add, Matrix.inv_mul_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
rw : q ⊓ p ≤ ⊥
⊢ Disjoint q p

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
⊢ q ⊓ p ≤ ⊥

Tactic:
fun i h => h.1 h.2

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
⊢ q ⊓ p ≤ ⊥

Tactic:
exact fun i h => h.1 h.2
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
⊢ M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0

Tactic:
have h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0 := by
    rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]
    rw [disjoint_iff_inf_le]
    exact fun i h => h.1 h.2
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
a : ∀ (i : { a : m // q a }) (j : { a : m // p a }), M.toBlock q p i j = 0 i j
⊢ M.toBlock q p = 0

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
i : { a : m // q a }
j : { a : m // p a }
⊢ M.toBlock q p i j = 0 i j

Tactic:
simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_gt i.2)

Premises used: le_of_not_gt, lt_of_lt_of_le, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
⊢ M.toBlock q p = 0

Tactic:
have h_zero : M.toBlock q p = 0 := by
    ext i j
    simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_gt i.2)
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
⊢ M⁻¹.toBlock q p * M.toBlock p p = 0

Tactic:
simpa [h_zero] using h_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
⊢ M⁻¹.toBlock q p * M.toBlock p p = 0

Tactic:
have h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0 := by simpa [h_zero] using h_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
haveI :
  ∀ (this : Invertible (M.toBlock p p)),
    Eq (α := Matrix.{u_3, u_3, v} { a : m // k ≤ b a } { a : m // b a < k } R)
      (M⁻¹.toBlock (fun (i : m) ↦ k ≤ b i) fun (i : m) ↦ b i < k) 0
⊢ Eq (α := Matrix.{u_3, u_3, v} { a : m // k ≤ b a } { a : m // b a < k } R)
    (M⁻¹.toBlock (fun (i : m) ↦ k ≤ b i) fun (i : m) ↦ b i < k) 0

Tactic:
haveI : Invertible (M.toBlock p p) := hM.invertibleToBlock k
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this : Invertible (M.toBlock p p)
h : ∀ (x : m), k ≤ b x ↔ q x
⊢ (fun (i : m) ↦ k ≤ b i) = q

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this : Invertible (M.toBlock p p)
x : m
⊢ k ≤ b x ↔ q x

Tactic:
not_lt.symm

Premises used: not_lt, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this : Invertible (M.toBlock p p)
x : m
⊢ k ≤ b x ↔ q x

Tactic:
exact not_lt.symm

Premises used: not_lt, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this : Invertible (M.toBlock p p)
⊢ (fun (i : m) ↦ k ≤ b i) = q

Tactic:
have : (fun i => k ≤ b i) = q := by
    ext
    exact not_lt.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
k : α
p : (i : m) → Prop := fun (i : m) ↦ b i < k
q : (i : m) → Prop := fun (i : m) ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this_1 : Invertible (M.toBlock p p)
this : (fun (i : m) ↦ k ≤ b i) = q
rw : Eq (α := Matrix.{u_3, u_3, v} (Subtype q) { a : m // b a < k } R) (M⁻¹.toBlock q fun (i : m) ↦ b i < k) 0
rw₁ : (M⁻¹.toBlock q fun (i : m) ↦ b i < k) = 0 * (M.toBlock p p)⁻¹
rw₂ : (M⁻¹.toBlock q fun (i : m) ↦ b i < k) = M⁻¹.toBlock q p * M.toBlock p p * (M.toBlock p p)⁻¹
rw₃ rw₄ : (M⁻¹.toBlock q fun (i : m) ↦ b i < k) = M⁻¹.toBlock q p
⊢ Eq (α := Matrix.{u_3, u_3, v} { a : m // k ≤ b a } { a : m // b a < k } R)
    (M⁻¹.toBlock (fun (i : m) ↦ k ≤ b i) fun (i : m) ↦ b i < k) 0

Tactic:
rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
    mul_inv_cancel_right_of_invertible]

Premises used: Matrix.toBlock, Matrix.mul_inv_cancel_right_of_invertible, Inv.inv, Matrix.zero_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
exact this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
suffices : ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
suffices ∀ hs : Finset α, univ.image b = hs → BlockTriangular M⁻¹ b by exact this _ rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
hs : image b univ = s
⊢ ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b

Tactic:
subst hs
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
H : ∀ (this : Inhabited m), M⁻¹ i j = 0
⊢ M⁻¹ i j = 0

Tactic:
haveI : Inhabited m := ⟨i⟩