awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
B : BilinForm R₂ M₂
b : Basis ι R₂ M₂
⊢ Matrix.SeparatingLeft.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
      ((toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B) ↔
    SeparatingLeft B

Tactic:
(Matrix.separatingLeft_toBilin_iff b).symm.trans <| (Matrix.toBilin_toMatrix b B).symm ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, Matrix.toBilin_toMatrix, Iff.trans, Matrix.separatingLeft_toBilin_iff, Eq.symm, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
B : BilinForm R₂ M₂
h : SeparatingLeft B
b : Basis ι R₂ M₂
⊢ Matrix.SeparatingLeft.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)

Tactic:
(separatingLeft_toMatrix_iff b).mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.separatingLeft_toMatrix_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
B : BilinForm R₂ (ι → R₂)
⊢ Matrix.SeparatingRight.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
      ((toMatrix' : (a : BilinForm R₂ (ι → R₂)) → Matrix ι ι R₂) B) ↔
    SeparatingRight B

Tactic:
Matrix.separatingRight_toBilin'_iff.symm.trans <| (Matrix.toBilin'_toMatrix' B).symm ▸ Iff.rfl

Premises used: Iff.trans, Matrix.separatingRight_toBilin'_iff, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
inst : CommRing R₂
ι : Type u_6
inst_1 : DecidableEq ι
inst_2 : Fintype ι
B : BilinForm R₂ (ι → R₂)
h : SeparatingRight B
⊢ Matrix.SeparatingRight.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix' : (a : BilinForm R₂ (ι → R₂)) → Matrix ι ι R₂) B)

Tactic:
separatingRight_toMatrix'_iff.mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.separatingRight_toMatrix'_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
B : BilinForm R₂ M₂
b : Basis ι R₂ M₂
⊢ Matrix.SeparatingRight.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
      ((toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B) ↔
    SeparatingRight B

Tactic:
(Matrix.separatingRight_toBilin_iff b).symm.trans <| (Matrix.toBilin_toMatrix b B).symm ▸ Iff.rfl

Premises used: Matrix.separatingRight_toBilin_iff, Iff.rfl, Eq.rec, Matrix.toBilin_toMatrix, Iff.trans, Eq.symm, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
R₂ : Type u_3
M₂ : Type u_4
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
ι : Type u_6
inst_3 : DecidableEq ι
inst_4 : Fintype ι
B : BilinForm R₂ M₂
h : SeparatingRight B
b : Basis ι R₂ M₂
⊢ Matrix.SeparatingRight.{u_6, u_6, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)

Tactic:
(separatingRight_toMatrix_iff b).mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.separatingRight_toMatrix_iff
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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
rw₁ rw₂ : M.det ≠ 0 ↔ M.det ≠ 0
⊢ Nondegenerate (R := A) (M := ι → A) ((toBilin' : (a : Matrix ι ι A) → BilinForm A (ι → A)) M) ↔ M.det ≠ 0

Tactic:
rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]

Premises used: Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
Goal:
A : Type u_5
inst : CommRing A
inst_1 : IsDomain A
ι : Type u_6
inst_2 : DecidableEq ι
inst_3 : Fintype ι
M : Matrix ι ι A
h : M.det ≠ 0
⊢ Nondegenerate (R := A) (M := ι → A) ((toBilin' : (a : Matrix ι ι A) → BilinForm A (ι → A)) M)

Tactic:
nondegenerate_toBilin'_iff_det_ne_zero.mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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)
rw₁ rw₂ : B.Nondegenerate ↔ B.Nondegenerate
⊢ B.Nondegenerate ↔
    Ne.{u_5 + 1} (α := A) (det.{u_5, u_6} (n := ι) ((toMatrix b : (a : BilinForm A M₂) → Matrix ι ι A) B)) 0

Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff]

Premises used: LinearMap.BilinForm.nondegenerate_toMatrix_iff, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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₂
B₃ : BilinForm A M₂
ι : Type u_6
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b : Basis ι A M₂
h : Ne.{u_5 + 1} (α := A) (det.{u_5, u_6} (n := ι) ((toMatrix b : (a : BilinForm A M₂) → Matrix ι ι A) B₃)) 0
⊢ B₃.Nondegenerate

Tactic:
(nondegenerate_iff_det_ne_zero b).mpr h

Premises used: Iff.mpr, LinearMap.BilinForm.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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
obtain : ∀ (ι : Type u_4) (b : Basis ι R₂ M₂), B.Nondegenerate
⊢ B.Nondegenerate

Tactic:
obtain ⟨ι, b⟩ := Module.Free.exists_basis R₂ M₂

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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₂
⊢ Finite ι

Tactic:
have : Finite ι := Module.Finite.finite_basis b
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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 ι
have : ∀ (this : Fintype ι), B.Nondegenerate
⊢ B.Nondegenerate

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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 ι
have : ∀ (this : DecidableEq ι), B.Nondegenerate
⊢ B.Nondegenerate

Tactic:
have : DecidableEq ι := Classical.decEq ι
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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
rwa₂ :
  Matrix.SeparatingLeft.{u_4, u_4, u_3} (m := ι) (n := ι) (R := R₂)
    ((BilinForm.toMatrix b : (a : BilinForm R₂ M₂) → Matrix ι ι R₂) B)
rwa₃ rwa₄ rwa₅ rwa₆ : SeparatingLeft B
⊢ B.Nondegenerate

Tactic:
rwa [← BilinForm.nondegenerate_toMatrix_iff b, Matrix.nondegenerate_iff_det_ne_zero,
    ← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix_iff]

Premises used: LinearMap.BilinForm.nondegenerate_toMatrix_iff, Matrix.separatingLeft_iff_det_ne_zero, LinearMap.BilinForm.separatingLeft_toMatrix_iff, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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 : SeparatingRight B
⊢ B.Nondegenerate

Tactic:
nondegenerate_flip_iff.mp <| .ofSeparatingLeft hB

Premises used: LinearMap.BilinForm.nondegenerate_flip_iff, LinearMap.BilinForm.Nondegenerate.ofSeparatingLeft, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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 = ⊥

Tactic:
⟨Nondegenerate.ker_eq_bot, fun h ↦ .ofSeparatingLeft ?_⟩

Premises used: LinearMap.BilinForm.Nondegenerate.ofSeparatingLeft, Iff.intro, LinearMap.BilinForm.Nondegenerate.ker_eq_bot
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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₂
refine : ∀ (h : ker B = ⊥), SeparatingLeft B
⊢ B.Nondegenerate ↔ ker B = ⊥

Tactic:
refine ⟨Nondegenerate.ker_eq_bot, fun h ↦ .ofSeparatingLeft ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.BilinearForm
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₂
h : ker B = ⊥
rwa rwa₁ rwa₂ rwa₃ : ker B = ⊥
⊢ SeparatingLeft B

Tactic:
rwa [separatingLeft_iff_ker_eq_bot]

Premises used: LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
b : m → α
inst : LT α
inst_1 : Zero R
f : n → m
h : M.BlockTriangular b
⊢ (M.submatrix f f).BlockTriangular (b ∘ f)

Tactic:
fun _ _ hij => h hij

Premises used: Matrix.submatrix, Matrix.BlockTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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))

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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))
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
⊢ 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 => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
⊢ BlockTriangular.{v, u_1, u_3} (m := m) (R := R)
    (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))
    (b ∘ (⇑e : (a : m) → n))

Tactic:
h.submatrix

Premises used: Matrix.BlockTriangular.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
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)
⊢ M.BlockTriangular (b ∘ (⇑e : (a : m) → n))

Tactic:
convert! h.submatrix

Premises used: Matrix.BlockTriangular.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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 =
    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:
simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]

Premises used: Equiv.symm_comp_self, Matrix.reindex_apply, Matrix.submatrix_id_id, Matrix.submatrix_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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} (m := n) (M.submatrix (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m))
    (Function.comp.{u_4 + 1, u_3 + 1, u_1 + 1} (β := m) (b ∘ (⇑e : (a : m) → n)) (⇑e.symm : (a : n) → m))

Tactic:
h.submatrix

Premises used: Matrix.BlockTriangular.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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))
h₁ : b = Function.comp.{u_4 + 1, u_3 + 1, u_1 + 1} (β := m) (b ∘ (⇑e : (a : m) → n)) (⇑e.symm : (a : n) → m)
⊢ BlockTriangular.{v, u_1, u_4} (R := R) ((reindex e e : (a : Matrix m m R) → Matrix n n R) M) b

Tactic:
convert! h.submatrix

Premises used: Matrix.BlockTriangular.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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))
⊢ b = Function.comp.{u_4 + 1, u_3 + 1, u_1 + 1} (β := m) (b ∘ (⇑e : (a : m) → n)) (⇑e.symm : (a : n) → m)

Tactic:
simp only [comp_assoc b e e.symm, Equiv.self_comp_symm, comp_id]

Premises used: Function.comp_id, Equiv.self_comp_symm, Equiv.symm, DFunLike.coe, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : LT α
inst_1 : Zero R
⊢ M.BlockTriangular b → Mᵀ.BlockTriangular (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ b)

Tactic:
swap

Premises used: Function.swap, Matrix.BlockTriangular, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
inst : LT α
inst_1 : Zero R
b : m → αᵒᵈ
⊢ Mᵀ.BlockTriangular b ↔ M.BlockTriangular (α := α) ((⇑ofDual : (a : αᵒᵈ) → α) ∘ b)

Tactic:
forall_comm

Premises used: forall_comm, Matrix.BlockTriangular, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : LT α
inst_1 : Zero R
⊢ BlockTriangular.{v, u_1, u_3} (R := R) 0 b

Tactic:
fun _ _ _ => rfl

Premises used: Matrix.BlockTriangular, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
rw₂ rw₃ : Eq.{v + 1} (α := R) 0 0
⊢ (-M) x x_1 = 0

Tactic:
rw [neg_apply, hM h, neg_zero]

Premises used: Matrix.neg_apply, neg_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
simp_rw₂ : HAdd.hAdd (α := R) 0 0 = 0
⊢ (M + N) i j = 0

Tactic:
simp_rw [Matrix.add_apply, hM h, hN h, zero_add]

Premises used: Matrix.add_apply, zero_add
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
simp_rw₂ : HSub.hSub (α := R) 0 0 = 0
⊢ (M - N) i j = 0

Tactic:
simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]

Premises used: sub_zero, Matrix.sub_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : LT α
S : Type u_9
F : Type u_10
inst_1 : FunLike F R S
inst_2 : Zero R
inst_3 : Zero S
inst_4 : ZeroHomClass F R S
f : F
h : M.BlockTriangular b
i j : m
lt : b j < b i
⊢ Eq.{u_9 + 1} (α := S) (M.map (⇑f : (a : R) → S) i j) 0

Tactic:
simp [h lt]
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
b : m → α
inst : LT α
inst_1 : Zero R
M : Matrix m m (Matrix n n R)
h : M.BlockTriangular b
i j : m × n
lt : LT.lt.{u_1} (α := α) ((fun (i : m × n) ↦ b i.1) j) ((fun (i : m × n) ↦ b i.1) i)
⊢ Eq.{v + 1} (α := R) ((Matrix.comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) M i j : R)
    (0 : R)

Tactic:
simp [h lt]
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : Preorder α
inst_1 : Zero R
inst_2 : DecidableEq m
d : m → R
⊢ (diagonal d).BlockTriangular b

Tactic:
fun _ _ h => diagonal_apply_ne' d fun h' => ne_of_lt h (congr_arg _ h')

Premises used: Matrix.diagonal_apply_ne', Matrix.BlockTriangular, congr_arg, ne_of_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m' : α → Type u_6
R : Type v
inst : Preorder α
inst_1 : Zero R
inst_2 : DecidableEq α
d : (i : α) → Matrix.{u_6, u_6, v} (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h :
  (Sigma.mk (β := fun (i : α) ↦ m' i) j j').fst (β := fun (i : α) ↦ m' i) <
    (Sigma.mk (β := fun (i : α) ↦ m' i) i i').fst (β := fun (i : α) ↦ m' i)
⊢ blockDiagonal' (m' := m') (n' := m') d (Sigma.mk (β := fun (i : α) ↦ m' i) i i')
      (Sigma.mk (β := fun (i : α) ↦ m' i) j j') =
    0

Tactic:
apply blockDiagonal'_apply_ne d i' j' fun h' => ne_of_lt h h'.symm

Premises used: Matrix.blockDiagonal'_apply_ne, Eq.symm, ne_of_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
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)
⊢ blockDiagonal d (i, i') (j, j') = 0

Tactic:
rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']

Premises used: Matrix.blockTriangular_blockDiagonal', Matrix.blockDiagonal'_eq_blockDiagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
⊢ 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:
h
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
⊢ 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:
exact h
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : Preorder α
inst_1 : Zero R
inst_2 : DecidableEq m
inst_3 : One R
⊢ BlockTriangular.{v, u_1, u_3} (R := R) 1 b

Tactic:
blockTriangular_diagonal _

Premises used: Matrix.blockTriangular_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
h : ¬(i = r ∧ j = s)
⊢ single i j c r s = 0

Tactic:
apply single_apply_of_ne

Premises used: Matrix.single_apply_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
hrs : b j < b i
⊢ False

Tactic:
(hij.trans_lt hrs).false

Premises used: LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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
hrs : b j < b i
⊢ False

Tactic:
exact (hij.trans_lt hrs).false

Premises used: LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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 j ≤ b i
c : R
⊢ LE.le (α := αᵒᵈ) (((⇑toDual : (a : α) → αᵒᵈ) ∘ b) i) (((⇑toDual : (a : α) → αᵒᵈ) ∘ b) j)

Tactic:
toDual_le_toDual.mpr hij

Premises used: Iff.mpr, OrderDual.toDual_le_toDual
-- Module: Mathlib.LinearAlgebra.Matrix.Block
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 j ≤ b i
c : R
⊢ LE.le (α := αᵒᵈ) (((⇑toDual : (a : α) → αᵒᵈ) ∘ b) i) (((⇑toDual : (a : α) → αᵒᵈ) ∘ b) j)

Tactic:
exact toDual_le_toDual.mpr hij

Premises used: Iff.mpr, OrderDual.toDual_le_toDual
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : Preorder α
inst_1 : CommRing R
inst_2 : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
⊢ (transvection i j c).BlockTriangular b

Tactic:
blockTriangular_one.add (blockTriangular_single hij c)

Premises used: Matrix.BlockTriangular.add, Matrix.transvection, Matrix.blockTriangular_single, Matrix.blockTriangular_one
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst : Preorder α
inst_1 : CommRing R
inst_2 : DecidableEq m
i j : m
hij : b j ≤ b i
c : R
⊢ (transvection i j c).BlockTriangular (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ b)

Tactic:
blockTriangular_one.add (blockTriangular_single' hij c)

Premises used: Matrix.BlockTriangular.add, Matrix.transvection, Matrix.blockTriangular_single', Matrix.blockTriangular_one
-- 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
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
⊢ (M * N) i j = 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- 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 → HMul.hMul (α := R) ((fun (j : m) ↦ M i j) k) ((fun (j_1 : m) ↦ N j_1 j) k) = 0
⊢ 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

Tactic:
_