awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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 : LinearOrder α
hM : M.BlockTriangular b
s : Finset α
hs : image b univ = s
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det
have H : ∀ (s : Finset α)
  (ih :
    ∀ s_1 ∈ s,
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m]
        (hM : M.BlockTriangular b) (hs : image b univ = s.erase s_1),
        M.det = ∏ a ∈ s.erase s_1, (M.toSquareBlock b a).det)
  {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] (hM : M.BlockTriangular b)
  (hs : image b univ = s), M.det = ∏ a ∈ s, (M.toSquareBlock b a).det
Tactic: induction s using Finset.eraseInduction generalizing m with | H s ih =>
  subst hs
  cases isEmpty_or_nonempty m
  · simp
  let k := (univ.image b).max' (univ_nonempty.image _)
  rw [twoBlockTriangular_det' M fun i => b i = k]
  · have : univ.image b = insert k ((univ.image b).erase k) := by
      rw [insert_erase]
      apply max'_mem
    rw [this, prod_insert (notMem_erase _ _)]
    refine congr_arg _ ?_
    let b' := fun i : { a // b a ≠ k } => b ↑i
    have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
    have hb' : image b' univ = (image b univ).erase k := by
      convert! image_subtype_ne_univ_eq_image_erase k b
    rw [ih _ (max'_mem _ _) h' hb']
    refine Finset.prod_congr rfl fun l hl => ?_
    let he : { a // b' a = l } ≃ { a // b a = l } :=
      haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
      Equiv.subtypeSubtypeEquivSubtype @hc
    rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]
    rfl
  · intro i hi j hj
    apply hM
    rw [hi]
    apply lt_of_le_of_ne _ hj
    exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))
Cleared hypotheses: m, M, b, inst_1, inst_2, hM, s, hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ k : α, (M.toSquareBlock b k).det
have refine : ∀ (a : α), Membership.mem (γ := Finset α) univ a → ∀ (ha : a ∉ image b univ), (M.toSquareBlock b a).det = 1
Tactic: refine h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ (M.toSquareBlock b a).det = 1
have this : IsEmpty.{max 1 (u_3 + 1)} { i : m // b i = a }
Tactic: have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ i : m, M i i
have haveI : ∀ (this : DecidableEq R), M.det = ∏ i : m, M i i
Tactic: haveI : DecidableEq R := Classical.decEq _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ i : m, M i i
have simp_rw : Eq.{v + 1} (α := R) (∏ a ∈ image id univ, (M.toSquareBlock id a).det) (∏ i : m, M i i)
Tactic: simp_rw [h.det, image_id, det_toSquareBlock_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
⊢ M.det = ∏ i : m, M i i
have simp_rw₁ : Eq.{v + 1} (α := R) (∏ x : m, (M.toSquareBlock id x).det) (∏ i : m, M i i)
Tactic: simp_rw [h.det, image_id, det_toSquareBlock_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have rw : Mᵀ.det = ∏ i : m, M i i
Tactic: rw [← det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
    (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
have 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
Tactic: rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
      Nat.le_of_eq (h_deg i)))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
    (∏ 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
have 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)
Tactic: convert! prod_const_one with x _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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 : 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)
have h : (p x).coeff (↑x : ℕ) = 1
Tactic: rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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)
have h₁ : (p x).coeff (p x).natDegree = 1
Tactic: rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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)
have h₂ : (p x).leadingCoeff = 1
Tactic: rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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)
have h₃ : Eq.{v + 1} (α := R) 1 1
Tactic: rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have rw : (M⁻¹ * M).toBlock p p = 1
Tactic: rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have rw₁ : Eq (α := Matrix.{u_3, u_3, v} { a : m // p a } { a : m // p a } R) (toBlock 1 p p) 1
Tactic: rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have rw₂ : Eq (α := Matrix.{u_3, u_3, v} { a : m // p a } { a : m // p a } R) 1 1
Tactic: rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have a : ∀ (i : { a : m // ¬p a }) (j : { a : m // p a }), M.toBlock (fun (i : m) ↦ ¬p i) p i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ 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
have 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
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))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have rw : Disjoint q p
Tactic: rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ Disjoint q p
have rw : q ⊓ p ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ 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
have h_sum : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have a : ∀ (i : { a : m // q a }) (j : { a : m // p a }), M.toBlock q p i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ 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
have h_zero : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ 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
have h_mul_eq_zero : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have 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
Tactic: haveI : Invertible (M.toBlock p p) := hM.invertibleToBlock k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have h : ∀ (x : m), k ≤ b x ↔ q x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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)
⊢ 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
have this₁ : (fun (i : m) ↦ k ≤ b i) = q
Tactic: have : (fun i => k ≤ b i) = q := by
    ext
    exact not_lt.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have 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
Tactic: rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
    mul_inv_cancel_right_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have rw₁ : (M⁻¹.toBlock q fun (i : m) ↦ b i < k) = 0 * (M.toBlock p p)⁻¹
Tactic: rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
    mul_inv_cancel_right_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)⁻¹
⊢ 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
have rw₂ : (M⁻¹.toBlock q fun (i : m) ↦ b i < k) = M⁻¹.toBlock q p * M.toBlock p p * (M.toBlock p p)⁻¹
Tactic: rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
    mul_inv_cancel_right_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)⁻¹
⊢ 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
have rw₃ : (M⁻¹.toBlock q fun (i : m) ↦ b i < k) = M⁻¹.toBlock q p
Tactic: rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
    mul_inv_cancel_right_of_invertible]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M⁻¹.BlockTriangular b
have suffices : ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b
Tactic: suffices ∀ hs : Finset α, univ.image b = hs → BlockTriangular M⁻¹ b by exact this _ rfl