awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
⊢ 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))
have 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))
Tactic: rw [← Matrix.det_reindex_self (Equiv.sumCompl p).symm M]
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
⊢ 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))
have 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))
Tactic: rw [det_apply', det_apply']
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
⊢ 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))
have 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)
Tactic: congr
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
⊢ 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)
have 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)
Tactic: ext σ
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : 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)
have 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
Tactic: congr
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
⊢ 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
have 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
Tactic: ext x
-- 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
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 }
⊢ (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
have 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
Tactic: generalize hy : σ x = y
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
x 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
have e_f : ∀ (val : { a : m // p a })
  (hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) = 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 (Sum.inl val) =
    fromBlocks (m := { 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) y (Sum.inl val)
Tactic: cases x
Cleared hypotheses: x, hy
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
x 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
e_f :
  ∀ (val : { a : m // p a })
    (hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) = 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 (Sum.inl val) =
      fromBlocks (m := { 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) y (Sum.inl val)
⊢ (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
have e_f₁ : ∀ (val : { a : m // ¬p a })
  (hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) = 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 (Sum.inr val) =
    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 (Sum.inr val)
Tactic: cases x
Cleared hypotheses: x, hy
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
y : { a : m // p a } ⊕ { a : m // ¬p a }
val : { a : m // p a }
hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) = 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 (Sum.inl val) =
    fromBlocks (m := { 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) y (Sum.inl val)
have e_f : ∀ (val_1 : { a : m // p a })
  (hy :
    Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
      ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
        { a : m // p a } ⊕ { a : m // ¬p a })
      (Sum.inl val_1 : { 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 (Sum.inl val_1) (Sum.inl val) =
    fromBlocks (m := { a : m // ¬p a }) (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) (Sum.inl val_1)
      (Sum.inl val)
Tactic: cases y
Cleared hypotheses: y, hy
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
y : { a : m // p a } ⊕ { a : m // ¬p a }
val : { a : m // p a }
hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) = y
e_f :
  ∀ (val_1 : { a : m // p a })
    (hy :
      Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
        ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
          { a : m // p a } ⊕ { a : m // ¬p a })
        (Sum.inl val_1 : { 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 (Sum.inl val_1) (Sum.inl val) =
      fromBlocks (m := { a : m // ¬p a }) (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) (Sum.inl val_1)
        (Sum.inl val)
⊢ (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 (Sum.inl val) =
    fromBlocks (m := { 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) y (Sum.inl val)
have e_f₁ : ∀ (val_1 : { a : m // ¬p a })
  (hy :
    Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
      ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
        { a : m // p a } ⊕ { a : m // ¬p a })
      (Sum.inr val_1 : { 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 (Sum.inr val_1) (Sum.inl val) =
    fromBlocks (m := { 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) (Sum.inr val_1)
      (Sum.inl val)
Tactic: cases y
Cleared hypotheses: y, hy
-- 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
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
y : { a : m // p a } ⊕ { a : m // ¬p a }
val : { a : m // ¬p a }
hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) = 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 (Sum.inr val) =
    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 (Sum.inr val)
have e_f : ∀ (val_1 : { a : m // p a })
  (hy :
    Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
      ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) :
        { a : m // p a } ⊕ { a : m // ¬p a })
      (Sum.inl val_1 : { 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 (Sum.inl val_1) (Sum.inr val) =
    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) (Sum.inl val_1)
      (Sum.inr val)
Tactic: cases y
Cleared hypotheses: y, hy