awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LinearOrder α
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
h : Membership.mem (γ := Finset m) univ k
pos : ∀ (hki : b k < b i), HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
neg : ∀ (hki : b i ≤ b k), HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0

Tactic:
by_cases! hki : b k < b i
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LinearOrder α
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
h : Membership.mem (γ := Finset m) univ k
hki : b k < b i
pos pos₁ : M i k * N k j = 0
pos₂ : 0 * N k j = 0
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0

Tactic:
simp_rw [hM hki, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LinearOrder α
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
h : Membership.mem (γ := Finset m) univ k
hki : b i ≤ b k
neg neg₁ : M i k * N k j = 0
neg₂ : M i k * 0 = 0
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0

Tactic:
simp_rw [hN (lt_of_lt_of_le hij hki), mul_zero]

Premises used: MulZeroClass.mul_zero, lt_of_lt_of_le
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LinearOrder α
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : Semiring R
M : Matrix m m R
⊢ Membership.mem (γ := Subsemiring (Matrix m m R)) (blockTriangularSubsemiring R b) M ↔ M.BlockTriangular b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Matrix.BlockTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : LinearOrder α
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : Semiring R
hM : M.BlockTriangular b
n : ℕ
⊢ (M ^ n).BlockTriangular b

Tactic:
pow_mem (S := blockTriangularSubsemiring R b) hM n

Premises used: Set.Mem, setOf, Matrix.BlockTriangular, pow_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
A : Type u_8
b : m → α
inst : LinearOrder α
inst_1 : CommSemiring R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : DecidableEq m
inst_5 : Fintype m
r : R
⊢ BlockTriangular.{u_8, u_1, u_3} (R := A) ((algebraMap R (Matrix m m A) : (a : R) → Matrix m m A) r) b

Tactic:
blockTriangular_diagonal _

Premises used: Matrix.blockTriangular_diagonal, Matrix.diagonal, ite
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
A : Type u_8
b : m → α
inst : LinearOrder α
inst_1 : CommSemiring R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : DecidableEq m
inst_5 : Fintype m
M : Matrix m m A
⊢ Membership.mem (γ := Subalgebra R (Matrix m m A)) (blockTriangularSubalgebra R A b) M ↔ M.BlockTriangular b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Matrix.BlockTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : m
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl c))
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0

Tactic:
simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : m
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl c))
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0

Tactic:
first | simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : m
d : n
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl c))
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0

Tactic:
simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : m
d : n
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl c))
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0

Tactic:
first | simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : n
d : m
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr c))
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0

Tactic:
simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : n
d : m
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inl d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr c))
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0

Tactic:
first | simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr c))
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0

Tactic:
simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst : Zero R
inst_1 : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd :
  LT.lt.{u_1} (α := α) (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr d))
    (Sum.elim (fun (x : m) ↦ a) (fun (x : n) ↦ b) (Sum.inr c))
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0

Tactic:
first | simp [hab.not_gt] at hcd ⊢

Premises used: LT.lt.not_gt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p q : m → Prop
inst_3 : DecidablePred p
inst_4 : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ det.{v, u_3} (n := { x : m // p x })
      ((reindex (Equiv.subtypeEquivRight (p := q) (q := p) e) (Equiv.subtypeEquivRight (p := q) (q := p) e) :
          (a : Matrix { x : m // q x } { x : m // q x } R) → Matrix { x : m // p x } { x : m // p x } R)
        (M.toSquareBlockProp q)) =
    (M.toSquareBlockProp q).det

Tactic:
Matrix.det_reindex_self (Equiv.subtypeEquivRight e)
      (toSquareBlockProp M q)

Premises used: Equiv.subtypeEquivRight, Matrix.det_reindex_self, Matrix.toSquareBlockProp
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p q : m → Prop
inst_3 : DecidablePred p
inst_4 : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ (M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det

Tactic:
convert!
    Matrix.det_reindex_self (Equiv.subtypeEquivRight e)
      (toSquareBlockProp M q)

Premises used: Equiv.subtypeEquivRight, Matrix.det_reindex_self, Matrix.toSquareBlockProp
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
i : m
⊢ (M.toSquareBlock id i).det = M i i

Tactic:
letI : Unique { a // id a = i } := ⟨⟨⟨i, rfl⟩⟩, fun j => Subtype.ext j.property⟩
  (det_unique _).trans rfl

Premises used: id, Matrix.det_unique, rfl, Eq.trans, Matrix.toSquareBlock
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
rw :
  det.{v, u_3} (n := { a : m // p a } ⊕ { a : m // ¬p a })
      ((reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M) =
    det (n := { a : m // p a } ⊕ { a : m // ¬p a })
      (fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j))
⊢ M.det =
    det (n := { a : m // p a } ⊕ { a : m // ¬p a })
      (fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j))

Tactic:
rw [← Matrix.det_reindex_self (Equiv.sumCompl p).symm M]

Premises used: Matrix.det_reindex_self, Equiv.sumCompl, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }),
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
              (a : Matrix m m R) →
                Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
            M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i))
    (∑ σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }),
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
            (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
            ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i))
⊢ det.{v, u_3} (n := { a : m // p a } ⊕ { a : m // ¬p a })
      ((reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M) =
    det (n := { a : m // p a } ⊕ { a : m // ¬p a })
      (fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j))

Tactic:
rw [det_apply', det_apply']

Premises used: Matrix.det_apply'
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
e_f :
  Eq (α := Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) → R)
    (fun (σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) ↦
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
              (a : Matrix m m R) →
                Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
            M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i))
    fun (σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) ↦
    HMul.hMul (α := R)
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                  (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                σ) :
            ℤ) :
        R)
      (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
        fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
          (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
          ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i)
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }),
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
              (a : Matrix m m R) →
                Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
            M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i))
    (∑ σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }),
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
            (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
            ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
e_f :
  ∀ (σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })),
    HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
              (a : Matrix m m R) →
                Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
            M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i) =
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
            (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
            ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i)
⊢ Eq (α := Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) → R)
    (fun (σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) ↦
      HMul.hMul (α := R)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                    (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                  σ) :
              ℤ) :
          R)
        (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
          (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
              (a : Matrix m m R) →
                Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
            M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i))
    fun (σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) ↦
    HMul.hMul (α := R)
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                  (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                σ) :
            ℤ) :
        R)
      (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
        fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
          (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
          ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i)

Tactic:
ext σ
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
e_f :
  Eq (α := { a : m // p a } ⊕ { a : m // ¬p a } → R)
    (fun (i : { a : m // p a } ⊕ { a : m // ¬p a }) ↦
      (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i)
    fun (i : { a : m // p a } ⊕ { a : m // ¬p a }) ↦
    fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
      ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i
⊢ HMul.hMul (α := R)
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                  (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                σ) :
            ℤ) :
        R)
      (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
        (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
            (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
          M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i) =
    HMul.hMul (α := R)
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a }) →* ℤˣ) :
                  (a : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })) → ℤˣ)
                σ) :
            ℤ) :
        R)
      (∏ i : { a : m // p a } ⊕ { a : m // ¬p a },
        fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
          (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
          ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
e_f :
  ∀ (x : { a : m // p a } ⊕ { a : m // ¬p a }),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) x) x =
      fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
        (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
        ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) x) x
⊢ Eq (α := { a : m // p a } ⊕ { a : m // ¬p a } → R)
    (fun (i : { a : m // p a } ⊕ { a : m // ¬p a }) ↦
      (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i)
    fun (i : { a : m // p a } ⊕ { a : m // ¬p a }) ↦
    fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
      ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) i) i

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
x : { a : m // p a } ⊕ { a : m // ¬p a }
e_f :
  ∀ (y : { a : m // p a } ⊕ { a : m // ¬p a })
    (hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) x = y),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M y x =
      fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) y x
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) x) x =
    fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)
      ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) x) x

Tactic:
generalize hy : σ x = y

Premises used: DFunLike.coe