awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B₂ : BilinForm R₁ (n → R₁)
rw :
  toBilin'Aux
      (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
              Pi.single (M := fun (j : n) ↦ R₁) j 1 :
            (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
rw₁ :
  toLinearMap₂'Aux (RingHom.id R₁) (RingHom.id R₁)
      (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
              Pi.single (M := fun (j : n) ↦ R₁) j 1 :
            (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
⊢ toBilin'Aux
      ((BilinForm.toMatrixAux fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1 :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
have rw₂ : B₂ = B₂
Tactic: rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, toLinearMap₂'Aux_toMatrix₂Aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := Matrix n n R₁ ≃ₗ[R₁] BilinForm R₁ (n → R₁)) (toBilin (Pi.basisFun R₁ n)) toBilin'
have h : ∀ (M : Matrix n n R₁) (i i_1 : n),
  Eq (α := R₁)
    ((((((toBilin (Pi.basisFun R₁ n) : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M ∘ₗ
                      LinearMap.single R₁ (fun (i : n) ↦ R₁) i :
                    R₁ →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) :
                  (a : R₁) → (n → R₁) →ₗ[R₁] R₁)
                1 ∘ₗ
              LinearMap.single R₁ (fun (i : n) ↦ R₁) i_1 :
            R₁ →ₗ[R₁] R₁) :
          (a : R₁) → R₁)
        1 :
      R₁)
    ((((((toBilin' : (a : Matrix n n R₁) → BilinForm R₁ (n → R₁)) M ∘ₗ LinearMap.single R₁ (fun (i : n) ↦ R₁) i :
                    R₁ →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) :
                  (a : R₁) → (n → R₁) →ₗ[R₁] R₁)
                1 ∘ₗ
              LinearMap.single R₁ (fun (i : n) ↦ R₁) i_1 :
            R₁ →ₗ[R₁] R₁) :
          (a : R₁) → R₁)
        1 :
      R₁)
Tactic: ext M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix (Pi.basisFun R₁ n)) toMatrix'
have rw : Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) toMatrix'
Tactic: rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
rw : Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) toMatrix'
⊢ Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix (Pi.basisFun R₁ n)) toMatrix'
have rw₁ : Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) (toMatrix₂' R₁)
Tactic: rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
rw : Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) toMatrix'
rw₁ :
  Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix₂ (Pi.basisFun R₁ n) (Pi.basisFun R₁ n)) (toMatrix₂' R₁)
⊢ Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁) (toMatrix (Pi.basisFun R₁ n)) toMatrix'
have rw₂ : Eq (α := BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁)
  (toMatrix₂' R₁ : ((n → R₁) →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) ≃ₗ[R₁] Matrix n n R₁)
  (toMatrix₂' R₁ : ((n → R₁) →ₗ[R₁] (n → R₁) →ₗ[R₁] R₁) ≃ₗ[R₁] Matrix n n R₁)
Tactic: rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
⊢ Eq (α := BilinForm R₁ M₂')
    (BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
      ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P) ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q))
    ((toBilin c : (a : Matrix o o R₁) → BilinForm R₁ M₂') (Pᵀ * M * Q))
have H : ∀ (x y : M₂'),
  Eq.{u_1 + 1} (α := R₁)
    ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
    ((((((toBilin c : (a : Matrix o o R₁) → BilinForm R₁ M₂') (Pᵀ * M * Q) : BilinForm R₁ M₂') :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
M₁ : Type u_2
inst : CommSemiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
n : Type u_5
o : Type u_6
inst_3 : Fintype n
inst_4 : Fintype o
inst_5 : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₁ M₂'
c : Basis o R₁ M₂'
inst_8 : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ Eq.{u_1 + 1} (α := R₁)
    ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toBilin b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                  ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
    ((((((toBilin c : (a : Matrix o o R₁) → BilinForm R₁ M₂') (Pᵀ * M * Q) : BilinForm R₁ M₂') :
                (a : M₂') → M₂' →ₗ[R₁] R₁)
              x :
            M₂' →ₗ[R₁] R₁) :
          (a : M₂') → R₁)
        y :
      R₁)
have H : Eq.{u_1 + 1} (α := R₁)
  ((((BilinForm.comp.{u_2, u_1, u_7} (M' := M₁) ((toLinearMap₂ b b : (a : Matrix n n R₁) → BilinForm R₁ M₁) M)
                ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
              (a : M₂') → M₂' →ₗ[R₁] R₁)
            x :
          M₂' →ₗ[R₁] R₁) :
        (a : M₂') → R₁)
      y :
    R₁)
  ((((compl₁₂.{u_1, u_1, u_2, u_2, u_1, u_7, u_7} (Mₗ := M₁) (N := M₁)
                ((toLinearMap₂ b b : (a : Matrix n n R₁) → M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁) M)
                ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) P)
                ((toLin c b : (a : Matrix n o R₁) → M₂' →ₗ[R₁] M₁) Q) :
              (a : M₂') → M₂' →ₗ[R₁] R₁)
            x :
          M₂' →ₗ[R₁] R₁) :
        (a : M₂') → R₁)
      y :
    R₁)
Tactic: rw [Matrix.toBilin, LinearMap.BilinForm.toMatrix, Matrix.toBilin, LinearMap.BilinForm.toMatrix,
    toMatrix₂_symm, toMatrix₂_symm, ← Matrix.toLinearMap₂_compl₁₂ b b c c]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
A : Type u_5
inst : CommRing A
inst_1 : IsDomain A
ι : Type u_6
inst_2 : DecidableEq ι
inst_3 : Fintype ι
M : Matrix ι ι A
⊢ Nondegenerate (R := A) (M := ι → A) ((toBilin' : (a : Matrix ι ι A) → BilinForm A (ι → A)) M) ↔ M.det ≠ 0
have rw : M.Nondegenerate ↔ M.det ≠ 0
Tactic: rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
A : Type u_5
inst : CommRing A
inst_1 : IsDomain A
ι : Type u_6
inst_2 : DecidableEq ι
inst_3 : Fintype ι
M : Matrix ι ι A
rw : M.Nondegenerate ↔ M.det ≠ 0
⊢ Nondegenerate (R := A) (M := ι → A) ((toBilin' : (a : Matrix ι ι A) → BilinForm A (ι → A)) M) ↔ M.det ≠ 0
have rw₁ : M.det ≠ 0 ↔ M.det ≠ 0
Tactic: rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
M₂ : Type u_4
inst : AddCommGroup M₂
A : Type u_5
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : Module A M₂
ι : Type u_6
inst_4 : DecidableEq ι
inst_5 : Fintype ι
B : BilinForm A M₂
b : Basis ι A M₂
⊢ B.Nondegenerate ↔
    Ne.{u_5 + 1} (α := A) (det.{u_5, u_6} (n := ι) ((toMatrix b : (a : BilinForm A M₂) → Matrix ι ι A) B)) 0
have rw : B.Nondegenerate ↔
  Matrix.Nondegenerate.{u_6, u_6, u_5} (m := ι) (n := ι) (R := A) ((toMatrix b : (a : BilinForm A M₂) → Matrix ι ι A) B)
Tactic: rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
M₂ : Type u_4
inst : AddCommGroup M₂
A : Type u_5
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : Module A M₂
ι : Type u_6
inst_4 : DecidableEq ι
inst_5 : Fintype ι
B : BilinForm A M₂
b : Basis ι A M₂
rw :
  B.Nondegenerate ↔
    Matrix.Nondegenerate.{u_6, u_6, u_5} (m := ι) (n := ι) (R := A)
      ((toMatrix b : (a : BilinForm A M₂) → Matrix ι ι A) B)
⊢ B.Nondegenerate ↔
    Ne.{u_5 + 1} (α := A) (det.{u_5, u_6} (n := ι) ((toMatrix b : (a : BilinForm A M₂) → Matrix ι ι A) B)) 0
have rw₁ : B.Nondegenerate ↔ B.Nondegenerate
Tactic: rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
⊢ B.Nondegenerate
have obtain : ∀ (ι : Type u_4) (b : Basis ι R₂ M₂), B.Nondegenerate
Tactic: obtain ⟨ι, b⟩ := Module.Free.exists_basis R₂ M₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (hypothesis)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
⊢ B.Nondegenerate
have this : Finite ι
Tactic: have : Finite ι := Module.Finite.finite_basis b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this : Finite ι
⊢ B.Nondegenerate
have have : ∀ (this : Fintype ι), B.Nondegenerate
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this_1 : Finite ι
this : Fintype ι
⊢ B.Nondegenerate
have have : ∀ (this : DecidableEq ι), B.Nondegenerate
Tactic: have : DecidableEq ι := Classical.decEq ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this_1 : Finite ι
this_2 : Fintype ι
this : DecidableEq ι
⊢ B.Nondegenerate
have rwa : Matrix.Nondegenerate.{u_4, u_4, u_3} (m := ι) (n := ι) (R := R₂)
  ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)
Tactic: rwa [← BilinForm.nondegenerate_toMatrix_iff b, Matrix.nondegenerate_iff_det_ne_zero,
    ← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this_1 : Finite ι
this_2 : Fintype ι
this : DecidableEq ι
rwa :
  Matrix.Nondegenerate.{u_4, u_4, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)
⊢ B.Nondegenerate
have rwa₁ : Ne.{u_3 + 1} (α := R₂)
  (Matrix.det.{u_3, u_4} (n := ι) ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)) 0
Tactic: rwa [← BilinForm.nondegenerate_toMatrix_iff b, Matrix.nondegenerate_iff_det_ne_zero,
    ← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this_1 : Finite ι
this_2 : Fintype ι
this : DecidableEq ι
rwa :
  Matrix.Nondegenerate.{u_4, u_4, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)
rwa₁ :
  Ne.{u_3 + 1} (α := R₂)
    (Matrix.det.{u_3, u_4} (n := ι) ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)) 0
⊢ B.Nondegenerate
have rwa₂ : Matrix.SeparatingLeft.{u_4, u_4, u_3} (m := ι) (n := ι) (R := R₂)
  ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)
Tactic: rwa [← BilinForm.nondegenerate_toMatrix_iff b, Matrix.nondegenerate_iff_det_ne_zero,
    ← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : IsDomain R₂
inst_4 : Free R₂ M₂
inst_5 : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
⊢ B.Nondegenerate ↔ ker B = ⊥
have refine : ∀ (h : ker B = ⊥), SeparatingLeft B
Tactic: refine ⟨Nondegenerate.ker_eq_bot, fun h ↦ .ofSeparatingLeft ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst : LT α
inst_1 : Zero R
b : n → α
e : m ≃ n
⊢ BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b ↔
    M.BlockTriangular (b ∘ (⇑e : (a : m) → n))
have refine_1 : ∀ (h : BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b),
  M.BlockTriangular (b ∘ (⇑e : (a : m) → n))
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst : LT α
inst_1 : Zero R
b : n → α
e : m ≃ n
refine_1 :
  ∀ (h : BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b),
    M.BlockTriangular (b ∘ (⇑e : (a : m) → n))
⊢ BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b ↔
    M.BlockTriangular (b ∘ (⇑e : (a : m) → n))
have refine_2 : ∀ (h : M.BlockTriangular (b ∘ (⇑e : (a : m) → n))),
  BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst : LT α
inst_1 : Zero R
b : n → α
e : m ≃ n
h : BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b
⊢ M.BlockTriangular (b ∘ (⇑e : (a : m) → n))
have h₁ : M =
  submatrix.{v, u_3, u_4, u_4, u_3} (m := n) (n := n) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M)
    (⇑e : (a : m) → n) (⇑e : (a : m) → n)
Tactic: convert! h.submatrix
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst : LT α
inst_1 : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ (⇑e : (a : m) → n))
⊢ BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b
have h₁ : b = Function.comp.{u_4 + 1, u_3 + 1, u_1 + 1} (β := m) (b ∘ (⇑e : (a : m) → n)) (⇑e.symm : (a : n) → m)
Tactic: convert! h.submatrix
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LT α
inst_1 : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x x_1 : m
h : b x_1 < b x
⊢ (-M) x x_1 = 0
have rw : -M x x_1 = 0
Tactic: rw [neg_apply, hM h, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LT α
inst_1 : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x x_1 : m
h : b x_1 < b x
rw : -M x x_1 = 0
⊢ (-M) x x_1 = 0
have rw₁ : Eq.{v + 1} (α := R) (-0) 0
Tactic: rw [neg_apply, hM h, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LT α
inst_1 : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x x_1 : m
h : b x_1 < b x
rw : -M x x_1 = 0
rw₁ : Eq.{v + 1} (α := R) (-0) 0
⊢ (-M) x x_1 = 0
have rw₂ : Eq.{v + 1} (α := R) 0 0
Tactic: rw [neg_apply, hM h, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst : LT α
inst_1 : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M + N) i j = 0
have simp_rw : M i j + N i j = 0
Tactic: simp_rw [Matrix.add_apply, hM h, hN h, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst : LT α
inst_1 : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
simp_rw : M i j + N i j = 0
⊢ (M + N) i j = 0
have simp_rw₁ : 0 + N i j = 0
Tactic: simp_rw [Matrix.add_apply, hM h, hN h, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst : LT α
inst_1 : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
simp_rw : M i j + N i j = 0
simp_rw₁ : 0 + N i j = 0
⊢ (M + N) i j = 0
have simp_rw₂ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: simp_rw [Matrix.add_apply, hM h, hN h, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst : LT α
inst_1 : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M - N) i j = 0
have simp_rw : M i j - N i j = 0
Tactic: simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst : LT α
inst_1 : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
simp_rw : M i j - N i j = 0
⊢ (M - N) i j = 0
have simp_rw₁ : 0 - N i j = 0
Tactic: simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst : LT α
inst_1 : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
simp_rw : M i j - N i j = 0
simp_rw₁ : 0 - N i j = 0
⊢ (M - N) i j = 0
have simp_rw₂ : HSub.hSub (α := R) 0 0 = 0
Tactic: simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
inst : Preorder α
inst_1 : Zero R
inst_2 : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0
have a : Sigma.fst (β := fun (i : α) ↦ m) (Sigma.mk (β := fun (i : α) ↦ m) j' j) <
  Sigma.fst (β := fun (i : α) ↦ m) (Sigma.mk (β := fun (i : α) ↦ m) i' i)
Tactic: rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : Preorder α
inst_1 : Zero R
inst_2 : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r s : m
hrs : b s < b r
⊢ single i j c r s = 0
have h : ¬(i = r ∧ j = s)
Tactic: apply single_apply_of_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ (M * N) i j = 0
have h : ∀ (x : m),
  Membership.mem (γ := Finset m) univ x → HMul.hMul (α := R) ((fun (j : m) ↦ M i j) x) ((fun (j_1 : m) ↦ N j_1 j) x) = 0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
have 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
Tactic: by_cases! hki : b k < b i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
have 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
Tactic: by_cases! hki : b k < b i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
have pos₂ : 0 * N k j = 0
Tactic: simp_rw [hM hki, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
have neg₂ : M i k * 0 = 0
Tactic: simp_rw [hN (lt_of_lt_of_le hij hki), mul_zero]