awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ A.IsHermitian
have a : ∀ (i j : n), Aᴴ i j = A i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ (A.map f).IsHermitian
have rw : (A.map f)ᴴ = A.map f
Tactic: rw [IsHermitian, ← conjTranspose_map f hf, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
rw : (A.map f)ᴴ = A.map f
⊢ (A.map f).IsHermitian
have rw₁ : Aᴴ.map f = A.map f
Tactic: rw [IsHermitian, ← conjTranspose_map f hf, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
rw : (A.map f)ᴴ = A.map f
rw₁ : Aᴴ.map f = A.map f
⊢ (A.map f).IsHermitian
have rw₂ : A.map f = A.map f
Tactic: rw [IsHermitian, ← conjTranspose_map f hf, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f).IsHermitian ↔ A.IsHermitian
have rw : (A.map f)ᴴ = A.map f ↔ A.IsHermitian
Tactic: rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
rw : (A.map f)ᴴ = A.map f ↔ A.IsHermitian
⊢ (A.map f).IsHermitian ↔ A.IsHermitian
have rw₁ : (A.map f)ᴴ = A.map f ↔ Aᴴ = A
Tactic: rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
rw : (A.map f)ᴴ = A.map f ↔ A.IsHermitian
rw₁ : (A.map f)ᴴ = A.map f ↔ Aᴴ = A
⊢ (A.map f).IsHermitian ↔ A.IsHermitian
have rw₂ : Aᴴ.map f = A.map f ↔ Aᴴ = A
Tactic: rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
rw : (A.map f)ᴴ = A.map f ↔ A.IsHermitian
rw₁ : (A.map f)ᴴ = A.map f ↔ Aᴴ = A
rw₂ : Aᴴ.map f = A.map f ↔ Aᴴ = A
⊢ (A.map f).IsHermitian ↔ A.IsHermitian
have rw₃ : Aᴴ = A ↔ Aᴴ = A
Tactic: rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᵀ.IsHermitian
have rw : (Aᵀ.map star)ᵀ = Aᵀ
Tactic: rw [IsHermitian, conjTranspose, transpose_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian
have rw : Aᵀᵀ.IsHermitian
Tactic: rw [← transpose_transpose A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
f : n ≃ m
⊢ IsHermitian.{u_1, u_3} (α := α) (n := m) ((Matrix.reindex f f : (a : Matrix n n α) → Matrix m m α) A)
have rw : IsHermitian.{u_1, u_3} (n := m) (A.submatrix (⇑f.symm : (a : m) → n) (⇑f.symm : (a : m) → n))
Tactic: rw [reindex_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix n n α
f : n ≃ m
⊢ IsHermitian.{u_1, u_3} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A) ↔ A.IsHermitian
have refine : ∀ (h : IsHermitian.{u_1, u_3} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A)), A.IsHermitian
Tactic: refine ⟨fun h ↦ ?_, (·.reindex f)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix m m (Matrix n n α)
⊢ IsHermitian (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
have rw : Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
  A.IsHermitian
Tactic: rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
⊢ IsHermitian (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
have rw₁ : Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
  Aᴴ = A
Tactic: rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᴴ = A
⊢ IsHermitian (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
have rw₂ : Eq (α := Matrix (m × n) (m × n) α)
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) Aᴴ : Matrix (m × n) (m × n) α)
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
  Aᴴ = A
Tactic: rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᴴ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᴴ = A
rw₂ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) Aᴴ : Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᴴ = A
⊢ IsHermitian (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian
have rw₃ : Aᴴ = A ↔ Aᴴ = A
Tactic: rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix m m (Matrix n n α)
⊢ IsHermitian (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'
have simp : (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), star (A a_1 a b_1 b) = A a a_1 b b_1) ↔
  ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'
Tactic: simp [IsHermitian.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ Cᴴ = B
have rw : Bᴴᴴ = B
Tactic: rw [← hBC, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
rw : Bᴴᴴ = B
⊢ Cᴴ = B
have rw₁ : B = B
Tactic: rw [← hBC, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (hypothesis)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ (Matrix.fromBlocks A B C D).IsHermitian
have hCB : Cᴴ = B
Tactic: have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
have rw : Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
rw : Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
have rw₁ : Matrix.fromBlocks Aᴴ Cᴴ C Dᴴ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
rw : Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks Aᴴ Cᴴ C Dᴴ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
have rw₂ : Matrix.fromBlocks Aᴴ B C Dᴴ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
rw : Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks Aᴴ Cᴴ C Dᴴ = Matrix.fromBlocks A B C D
rw₂ : Matrix.fromBlocks Aᴴ B C Dᴴ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
have rw₃ : Matrix.fromBlocks A B C Dᴴ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
rw : Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks Aᴴ Cᴴ C Dᴴ = Matrix.fromBlocks A B C D
rw₂ : Matrix.fromBlocks Aᴴ B C Dᴴ = Matrix.fromBlocks A B C D
rw₃ : Matrix.fromBlocks A B C Dᴴ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
have rw₄ : Matrix.fromBlocks A B C D = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : CommMonoid α
inst_1 : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ (A ⊙ B).IsHermitian
have rw : (A ⊙ B)ᴴ = A ⊙ B
Tactic: rw [IsHermitian, conjTranspose_hadamard, hB.eq, hA.eq, hadamard_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : CommMonoid α
inst_1 : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
rw : (A ⊙ B)ᴴ = A ⊙ B
⊢ (A ⊙ B).IsHermitian
have rw₁ : Bᴴ ⊙ Aᴴ = A ⊙ B
Tactic: rw [IsHermitian, conjTranspose_hadamard, hB.eq, hA.eq, hadamard_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : CommMonoid α
inst_1 : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
rw : (A ⊙ B)ᴴ = A ⊙ B
rw₁ : Bᴴ ⊙ Aᴴ = A ⊙ B
⊢ (A ⊙ B).IsHermitian
have rw₂ : B ⊙ Aᴴ = A ⊙ B
Tactic: rw [IsHermitian, conjTranspose_hadamard, hB.eq, hA.eq, hadamard_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : CommMonoid α
inst_1 : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
rw : (A ⊙ B)ᴴ = A ⊙ B
rw₁ : Bᴴ ⊙ Aᴴ = A ⊙ B
rw₂ : B ⊙ Aᴴ = A ⊙ B
⊢ (A ⊙ B).IsHermitian
have rw₃ : B ⊙ A = A ⊙ B
Tactic: rw [IsHermitian, conjTranspose_hadamard, hB.eq, hA.eq, hadamard_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : CommMonoid α
inst_1 : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
rw : (A ⊙ B)ᴴ = A ⊙ B
rw₁ : Bᴴ ⊙ Aᴴ = A ⊙ B
rw₂ : B ⊙ Aᴴ = A ⊙ B
rw₃ : B ⊙ A = A ⊙ B
⊢ (A ⊙ B).IsHermitian
have rw₄ : A ⊙ B = A ⊙ B
Tactic: rw [IsHermitian, conjTranspose_hadamard, hB.eq, hA.eq, hadamard_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
⊢ (-A).IsHermitian ↔ A.IsHermitian
have refine : ∀ (h : (-A).IsHermitian), A.IsHermitian
Tactic: refine ⟨fun h ↦ ?_, (·.neg)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
n : Type u_4
inst : AddGroup α
inst_1 : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ A.IsHermitian
have rw : (- -A).IsHermitian
Tactic: rw [← neg_neg A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (k • A).IsHermitian
have rw : (k • A)ᴴ = k • A
Tactic: rw [IsHermitian, conjTranspose_smul, hk.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (k • A).IsHermitian
have rw₁ : star k • Aᴴ = k • A
Tactic: rw [IsHermitian, conjTranspose_smul, hk.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (k • A).IsHermitian
have rw₂ : k • Aᴴ = k • A
Tactic: rw [IsHermitian, conjTranspose_smul, hk.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (k • A).IsHermitian
have rw₃ : k • A = k • A
Tactic: rw [IsHermitian, conjTranspose_smul, hk.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (hypothesis)
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
⊢ A.IsHermitian
have h₁ : k • Aᴴ = k • A
Tactic: rw [IsHermitian, conjTranspose_smul, hk.star_eq] at h
Cleared hypotheses: h, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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 _)
⊢ A.IsHermitian
have rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsHermitian
Tactic: rw [← invOf_smul_smul k A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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 α
⊢ (A * Aᴴ).IsHermitian
have rw : (A * Aᴴ)ᴴ = A * Aᴴ
Tactic: rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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ᴴ
⊢ (A * Aᴴ).IsHermitian
have rw₁ : Aᴴᴴ * Aᴴ = A * Aᴴ
Tactic: rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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ᴴ
⊢ (A * Aᴴ).IsHermitian
have rw₂ : A * Aᴴ = A * Aᴴ
Tactic: rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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 α
⊢ (Aᴴ * A).IsHermitian
have rw : (Aᴴ * A)ᴴ = Aᴴ * A
Tactic: rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (Aᴴ * A).IsHermitian
have rw₁ : Aᴴ * Aᴴᴴ = Aᴴ * A
Tactic: rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (Aᴴ * A).IsHermitian
have rw₂ : Aᴴ * A = Aᴴ * A
Tactic: rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
have rw : A⁻¹⁻¹.IsHermitian
Tactic: rw [← inv_inv_of_invertible A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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 : ℤ
⊢ (A ^ k).IsHermitian
have rw : (A ^ k)ᴴ = A ^ k
Tactic: rw [IsHermitian, conjTranspose_zpow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (A ^ k).IsHermitian
have rw₁ : Aᴴ ^ k = A ^ k
Tactic: rw [IsHermitian, conjTranspose_zpow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (A ^ k).IsHermitian
have rw₂ : A ^ k = A ^ k
Tactic: rw [IsHermitian, conjTranspose_zpow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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 ⊕ᵥ 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
have 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)
Tactic: simp [Function.star_sumElim, vecMul_fromBlocks, add_vecMul,
    dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, hA.eq,
    conjTranspose_nonsing_inv, star_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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 ⊕ᵥ 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
have 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)
Tactic: simp [Function.star_sumElim, vecMul_fromBlocks, add_vecMul,
    dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, hD.eq,
    conjTranspose_nonsing_inv, star_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (hypothesis)
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
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
Tactic: have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := isHermitian_conjTranspose_mul_mul _ hA.inv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
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
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
have rw : A.IsHermitian ∧ Bᴴ = Bᴴ ∧ Bᴴᴴ = B ∧ D.IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
Tactic: rw [isHermitian_fromBlocks_iff]