awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
h : A.IsHermitian
⊢ (-A).IsHermitian

Tactic:
IsSelfAdjoint.neg h

Premises used: IsSelfAdjoint, Matrix.IsHermitian, IsSelfAdjoint.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
⊢ (-A).IsHermitian ↔ A.IsHermitian

Tactic:
⟨fun h ↦ ?_, (·.neg)⟩

Premises used: Matrix.IsHermitian.neg, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
refine : ∀ (h : (-A).IsHermitian), A.IsHermitian
⊢ (-A).IsHermitian ↔ A.IsHermitian

Tactic:
refine ⟨fun h ↦ ?_, (·.neg)⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
rw : (- -A).IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← neg_neg A]

Premises used: neg_neg
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ (- -A).IsHermitian

Tactic:
h.neg

Premises used: Matrix.IsHermitian.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ (- -A).IsHermitian

Tactic:
exact h.neg

Premises used: Matrix.IsHermitian.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ (A - B).IsHermitian

Tactic:
IsSelfAdjoint.sub hA hB

Premises used: IsSelfAdjoint, IsSelfAdjoint.sub, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Star R
inst_1 : Star α
inst_2 : SMul R α
inst_3 : StarModule R α
A : Matrix n n α
h : A.IsHermitian
k : R
hk : IsSelfAdjoint k
rw : (k • A)ᴴ = k • A
rw₁ : star k • Aᴴ = k • A
rw₂ : k • Aᴴ = k • A
rw₃ rw₄ : k • A = k • A
⊢ (k • A).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_smul, hk.star_eq, h.eq]

Premises used: Matrix.IsHermitian.eq, Matrix.IsHermitian, Matrix.conjTranspose_smul, IsSelfAdjoint.star_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint k
⊢ k • Aᴴ = k • A

Tactic:
rw [IsHermitian, conjTranspose_smul, hk.star_eq] at h

Premises used: Matrix.IsHermitian, Matrix.conjTranspose_smul, IsSelfAdjoint.star_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint k
h₁ : k • Aᴴ = k • A
⊢ IsSelfAdjoint k

Tactic:
rw [IsHermitian, conjTranspose_smul, hk.star_eq] at h

Premises used: Matrix.IsHermitian, Matrix.conjTranspose_smul, IsSelfAdjoint.star_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
h : k • Aᴴ = k • A
hk : IsSelfAdjoint k
⊢ A.IsHermitian

Tactic:
simpa using congr(⅟k • $h)
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _)
rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← invOf_smul_smul k A]

Premises used: invOf_smul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _)
⊢ (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsHermitian

Tactic:
h.smul hk

Premises used: Matrix.IsHermitian.smul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _)
⊢ (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsHermitian

Tactic:
exact h.smul hk

Premises used: Matrix.IsHermitian.smul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Star R
inst_2 : Star α
inst_3 : MulAction R α
inst_4 : StarModule R α
A : Matrix n n α
k : R
inst_5 : Invertible k
hk : IsSelfAdjoint k
⊢ (k • A).IsHermitian ↔ A.IsHermitian

Tactic:
⟨(·.of_smul hk), (·.smul hk)⟩

Premises used: Matrix.IsHermitian.of_smul, Matrix.IsHermitian.smul, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : NonUnitalSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
A : Matrix m n α
rw : (A * Aᴴ)ᴴ = A * Aᴴ
rw₁ : Aᴴᴴ * Aᴴ = A * Aᴴ
rw₂ rw₃ : A * Aᴴ = A * Aᴴ
⊢ (A * Aᴴ).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]

Premises used: Matrix.IsHermitian, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : NonUnitalSemiring α
inst_1 : StarRing α
inst_2 : Fintype m
A : Matrix m n α
rw : (Aᴴ * A)ᴴ = Aᴴ * A
rw₁ : Aᴴ * Aᴴᴴ = Aᴴ * A
rw₂ rw₃ : Aᴴ * A = Aᴴ * A
⊢ (Aᴴ * A).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]

Premises used: Matrix.IsHermitian, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : NonUnitalSemiring α
inst_1 : StarRing α
inst_2 : Fintype m
A : Matrix m m α
B : Matrix m n α
hA : A.IsHermitian
⊢ (Bᴴ * A * B).IsHermitian

Tactic:
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]

Premises used: Matrix.IsHermitian.eq, Matrix.mul_assoc, Matrix.IsHermitian, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : NonUnitalSemiring α
inst_1 : StarRing α
inst_2 : Fintype m
A : Matrix m m α
B : Matrix n m α
hA : A.IsHermitian
⊢ (B * A * Bᴴ).IsHermitian

Tactic:
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]

Premises used: Matrix.IsHermitian.eq, Matrix.mul_assoc, Matrix.IsHermitian, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : NonUnitalSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ Commute A B ↔ (A * B).IsHermitian

Tactic:
hA.isSelfAdjoint.commute_iff hB.isSelfAdjoint

Premises used: IsSelfAdjoint, Matrix.IsHermitian.isSelfAdjoint, IsSelfAdjoint.commute_iff, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : NonAssocSemiring α
inst_1 : StarRing α
inst_2 : DecidableEq n
⊢ IsHermitian.{u_1, u_4} (α := α) (n := n) 1

Tactic:
conjTranspose_one

Premises used: Matrix.conjTranspose_one, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Semiring α
inst_1 : StarRing α
inst_2 : DecidableEq n
d : ℕ
⊢ IsHermitian.{u_1, u_4} (α := α) (n := n) (↑d : Matrix n n α)

Tactic:
conjTranspose_natCast _

Premises used: Matrix.conjTranspose_natCast, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Semiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
h : A.IsHermitian
k : ℕ
⊢ (A ^ k).IsHermitian

Tactic:
IsSelfAdjoint.pow h _

Premises used: IsSelfAdjoint, Matrix.IsHermitian, IsSelfAdjoint.pow
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Ring α
inst_1 : StarRing α
inst_2 : DecidableEq n
d : ℤ
⊢ IsHermitian.{u_1, u_4} (α := α) (n := n) (↑d : Matrix n n α)

Tactic:
conjTranspose_intCast _

Premises used: Matrix.IsHermitian, Matrix.conjTranspose_intCast
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian

Tactic:
simp [IsHermitian, conjTranspose_nonsing_inv, hA.eq]

Premises used: Matrix.IsHermitian.eq, Matrix.conjTranspose_nonsing_inv, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
inst_4 : Invertible A
h : A⁻¹.IsHermitian
rw : A⁻¹⁻¹.IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← inv_inv_of_invertible A]

Premises used: Matrix.inv_inv_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
inst_4 : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian

Tactic:
IsHermitian.inv h

Premises used: Matrix.IsHermitian.inv
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
inst_4 : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian

Tactic:
exact IsHermitian.inv h

Premises used: Matrix.IsHermitian.inv
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
hA : A.IsHermitian
⊢ A.adjugate.IsHermitian

Tactic:
simp [IsHermitian, adjugate_conjTranspose, hA.eq]

Premises used: Matrix.IsHermitian.eq, Matrix.adjugate_conjTranspose, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
rw : (A ^ k)ᴴ = A ^ k
rw₁ : Aᴴ ^ k = A ^ k
rw₂ rw₃ : A ^ k = A ^ k
⊢ (A ^ k).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_zpow, h]

Premises used: Matrix.conjTranspose_zpow, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Fintype n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst_5 : Invertible A
hA : A.IsHermitian
simp :
  star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)
⊢ star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) =
    star (x + (A⁻¹ * B) *ᵥ y) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B) *ᵥ y) + star y ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y

Tactic:
simp [Function.star_sumElim, vecMul_fromBlocks, add_vecMul,
    dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, hA.eq,
    conjTranspose_nonsing_inv, star_mulVec]

Premises used: Matrix.IsHermitian.eq, Matrix.mul_assoc, Matrix.conjTranspose_nonsing_inv, Matrix.vecMul_fromBlocks, Matrix.add_vecMul, Function.star_sumElim, Matrix.vecMul_sub, Matrix.dotProduct_mulVec, Matrix.star_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Fintype n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst_5 : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst_5 : Invertible D
hD : D.IsHermitian
simp :
  star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)
⊢ star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) =
    star ((D⁻¹ * Bᴴ) *ᵥ x + y) ᵥ* D ⬝ᵥ ((D⁻¹ * Bᴴ) *ᵥ x + y) + star x ᵥ* (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x

Tactic:
simp [Function.star_sumElim, vecMul_fromBlocks, add_vecMul,
    dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, hD.eq,
    conjTranspose_nonsing_inv, star_mulVec]

Premises used: Matrix.IsHermitian.eq, Matrix.mul_assoc, Matrix.conjTranspose_nonsing_inv, Matrix.vecMul_fromBlocks, Matrix.add_vecMul, Function.star_sumElim, Matrix.vecMul_sub, Matrix.dotProduct_mulVec, Matrix.star_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst_5 : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hA : A.IsHermitian
⊢ (Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := isHermitian_conjTranspose_mul_mul _ hA.inv
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
rw : A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
rw [isHermitian_fromBlocks_iff]

Premises used: Matrix.isHermitian_fromBlocks_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
⟨fun h ↦ h.2.2.2.sub hBAB, fun h ↦ ⟨hA, rfl, conjTranspose_conjTranspose B,
    sub_add_cancel D _ ▸ h.add hBAB⟩⟩

Premises used: HMul.hMul, Matrix.IsHermitian.add, Eq.rec, Inv.inv, And.right, And.intro, Iff.intro, Matrix.IsHermitian.sub, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose, sub_add_cancel, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
exact ⟨fun h ↦ h.2.2.2.sub hBAB, fun h ↦ ⟨hA, rfl, conjTranspose_conjTranspose B,
    sub_add_cancel D _ ▸ h.add hBAB⟩⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
rw : (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
rw [← isHermitian_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
    fromBlocks_submatrix_sum_swap_sum_swap]

Premises used: Matrix.fromBlocks_submatrix_sum_swap_sum_swap, Equiv.sumComm, Matrix.isHermitian_submatrix_equiv, Equiv.sumComm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ (Matrix.fromBlocks D Bᴴ Bᴴᴴ A).IsHermitian ↔ (A - Bᴴᴴ * D⁻¹ * Bᴴ).IsHermitian

Tactic:
IsHermitian.fromBlocks₁₁ _ _ hD

Premises used: Matrix.IsHermitian.fromBlocks₁₁
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
h : B = Bᴴᴴ
h₁ : B = Bᴴᴴ
⊢ (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
convert! IsHermitian.fromBlocks₁₁ _ _ hD

Premises used: Matrix.IsHermitian.fromBlocks₁₁
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ B = Bᴴᴴ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : Membership.mem (γ := Set (Matrix n n R)) (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup I.matrix)) N
i j : n
rw : ∑ j_1 : n, M i j_1 * N j_1 j ∈ (↑I.toAddSubmonoid : Set R)
⊢ (M • N) i j ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
rw [smul_eq_mul, mul_apply]

Premises used: Matrix.mul_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : Membership.mem (γ := Set (Matrix n n R)) (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup I.matrix)) N
i j : n
h : ∀ (c : n), Membership.mem (γ := Finset n) Finset.univ c → M i c * N c j ∈ I.toAddSubmonoid
⊢ ∑ j_1 : n, M i j_1 * N j_1 j ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : Membership.mem (γ := Set (Matrix n n R)) (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup I.matrix)) N
i j k : n
h : Membership.mem (γ := Finset n) Finset.univ k → M i k * N k j ∈ I.toAddSubmonoid
⊢ Membership.mem (γ := Finset n) Finset.univ k → M i k * N k j ∈ I.toAddSubmonoid

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : Membership.mem (γ := Set (Matrix n n R)) (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup I.matrix)) N
i j k : n
h : Membership.mem (γ := Finset n) Finset.univ k
⊢ M i k * N k j ∈ I.toAddSubmonoid

Tactic:
apply I.mul_mem_left _ (hN k j)

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
⊢ Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) M ↔ ∀ (i j : n), M i j ∈ I

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Monotone (α := Ideal R) (β := Ideal (Matrix n n R)) (matrix n)

Tactic:
fun _ _ IJ _ MI i j => IJ (MI i j)

Premises used: Set.Mem, Monotone, setOf, Set.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
I J : Ideal R
eq : Eq (α := Ideal (Matrix n n R)) (matrix n I) (matrix n J)
h : ∀ (x : R), x ∈ I ↔ x ∈ J
⊢ I = J

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
I J : Ideal R
eq : Eq (α := Ideal (Matrix n n R)) (matrix n I) (matrix n J)
x : R
⊢ (∀ (x_1 x_2 : n), x ∈ I) ↔ ∀ (x_1 x_2 : n), x ∈ J

Tactic:
have : (∀ _ _, x ∈ I) ↔ (∀ _ _, x ∈ J) := congr((Matrix.of fun _ _ => x) ∈ $eq)
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
I J : Ideal R
eq : Eq (α := Ideal (Matrix n n R)) (matrix n I) (matrix n J)
x : R
this : (∀ (x_1 x_2 : n), x ∈ I) ↔ ∀ (x_1 x_2 : n), x ∈ J
⊢ x ∈ I ↔ x ∈ J

Tactic:
simpa only [forall_const] using this

Premises used: forall_const
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
h :
  ∀ (M : Matrix n n R),
    Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊥) M ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊥ M
⊢ Eq (α := Ideal (Matrix n n R)) (matrix n ⊥) ⊥

Tactic:
ext M
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
h : (∀ (i j : n), M i j = 0) ↔ M = 0
⊢ Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊥) M ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊥ M

Tactic:
simp only [mem_matrix, mem_bot]

Premises used: Ideal.mem_bot, Ideal.mem_matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
h : (∀ (i j : n), M i j = 0) → M = 0
h₁ : M = 0 → ∀ (i j : n), M i j = 0
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
h : ∀ (i j : n), M i j = 0 i j
⊢ M = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
i j : n
⊢ M i j = 0 i j

Tactic:
apply H
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
H : M = 0
⊢ ∀ (i j : n), M i j = 0

Tactic:
simp [H]
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
h :
  ∀ (x : Matrix n n R),
    Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊤) x ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊤ x
⊢ Eq (α := Ideal (Matrix n n R)) (matrix n ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n R
⊢ Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊤) x ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊤ x

Tactic:
simp