awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
i j x : n
a : v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
⊢ v (i - x) * w (x - j) =
    w (HSub.hSub (β := n) i (((Equiv.subLeft i).trans (Equiv.addRight j) : (a : n) → n) x : n)) *
      v (HSub.hSub (α := n) (((Equiv.subLeft i).trans (Equiv.addRight j) : (a : n) → n) x : n) j)

Tactic:
simp only [Equiv.trans_apply, Equiv.subLeft_apply, Equiv.coe_addRight, add_sub_cancel_right,
    mul_comm]

Premises used: Equiv.trans_apply, Equiv.coe_addRight, mul_comm, Equiv.subLeft_apply, add_sub_cancel_right
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
i j x : n
a : x - j = i - (i - x + j)
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))

Tactic:
congr 2
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : CommMagma α
inst_1 : AddCommMonoid α
inst_2 : Fintype n
inst_3 : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
inst : CommMagma α
inst_1 : AddCommMonoid α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant w * circulant v

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
R : Type u_4
inst : Sub n
inst_1 : SMul R α
k : R
v : n → α
⊢ circulant (k • v) = k • circulant v

Tactic:
rfl

Premises used: Matrix.circulant, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
n : Type u_6
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq n
inst_3 : AddGroup n
a : ∀ (i j : n), Eq.{u_5 + 1} (α := α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 1) i j) (1 i j)
⊢ Eq (α := Matrix n n α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 1)) 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
n : Type u_6
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq n
inst_3 : AddGroup n
i j : n
⊢ Eq.{u_5 + 1} (α := α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 1) i j) (1 i j)

Tactic:
simp [one_apply, Pi.single_apply, sub_eq_zero]

Premises used: Matrix.one_apply, sub_eq_zero, Pi.single_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_5
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : AddGroup n
inst_3 : Fintype n
a : α
a₁ :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 a) i j : α)
      ((scalar n : (a : α) → Matrix n n α) a i j : α)
⊢ Eq (α := Matrix n n α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 a)) ((scalar n : (a : α) → Matrix n n α) a)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_5
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : AddGroup n
inst_3 : Fintype n
a : α
i j : n
⊢ Eq.{u_1 + 1} (α := α) (circulant (Pi.single (M := fun (a : n) ↦ α) 0 a) i j : α)
    ((scalar n : (a : α) → Matrix n n α) a i j : α)

Tactic:
simp [Pi.single_apply, diagonal_apply, sub_eq_zero]

Premises used: sub_eq_zero, Pi.single_apply, Matrix.diagonal_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
inst : Zero α
inst_1 : One α
⊢ Eq.{u_5 + 1} (α := Matrix (Fin 0) (Fin 0) α) (circulant fun (i : Fin 0) ↦ if (↑i : ℕ) = 0 then 1 else 0) 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
inst : Zero α
inst_1 : One α
n : ℕ
rw :
  Eq.{u_5 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) α)
    (circulant fun (i : Fin (n + 1)) ↦ if (↑i : ℕ) = 0 then 1 else 0)
    (circulant (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1))
⊢ Eq.{u_5 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) α)
    (circulant fun (i : Fin (n + 1)) ↦ if (↑i : ℕ) = 0 then 1 else 0) 1

Tactic:
rw [← circulant_single_one]

Premises used: Matrix.circulant_single_one
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
inst : Zero α
inst_1 : One α
n : ℕ
e_v :
  ∀ (j : Fin (n + 1)),
    Eq.{u_5 + 1} (α := α) (if (↑j : ℕ) = 0 then 1 else 0 : α) (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1 j : α)
⊢ Eq.{u_5 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) α)
    (circulant fun (i : Fin (n + 1)) ↦ if (↑i : ℕ) = 0 then 1 else 0)
    (circulant (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1))

Tactic:
congr with j
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_5
inst : Zero α
inst_1 : One α
n : ℕ
j : Fin (n + 1)
⊢ Eq.{u_5 + 1} (α := α) (if (↑j : ℕ) = 0 then 1 else 0 : α) (Pi.single (M := fun (a : Fin (n + 1)) ↦ α) 0 1 j : α)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
rw : (circulant v)ᵀ = circulant v ↔ ∀ (i : n), v (-i) = v i
rw₁ : (circulant fun (i : n) ↦ v (-i)) = circulant v ↔ ∀ (i : n), v (-i) = v i
rw₂ : (fun (i : n) ↦ v (-i)) = v ↔ ∀ (i : n), v (-i) = v i
rw₃ rw₄ : (∀ (x : n), v (-x) = v x) ↔ ∀ (i : n), v (-i) = v i
⊢ (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i

Tactic:
rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]

Premises used: Matrix.transpose_circulant, funext_iff, Matrix.circulant_inj, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
v : Fin 0 → α
⊢ (circulant v).IsSymm ↔ ∀ (i : Fin 0), v (-i) = v i

Tactic:
simp [IsSymm.ext_iff, IsEmpty.forall_iff]

Premises used: Matrix.IsSymm.ext_iff, IsEmpty.forall_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
h : (circulant v).IsSymm
i : n
⊢ v (-i) = v i

Tactic:
circulant_isSymm_iff.1 h i

Premises used: Iff.mp, Matrix.circulant_isSymm_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Circulant
Goal:
α : Type u_1
n : ℕ
v : Fin n → α
h : (circulant v).IsSymm
i : Fin n
⊢ v (-i) = v i

Tactic:
Fin.circulant_isSymm_iff.1 h i

Premises used: Iff.mp, Matrix.Fin.circulant_isSymm_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : DecidableEq m
inst_2 : AddMonoid α
inst_3 : StarAddMonoid α
i : m
j : n
a : α
change : (single i j a)ᵀ.map (⇑starAddEquiv : (a : α) → α) = single j i (star a)
⊢ (single i j a)ᴴ = single j i (star a)

Tactic:
change (single i j a).transpose.map starAddEquiv = single j i (star a)

Premises used: Matrix.transpose, Matrix.map, starAddEquiv, DFunLike.coe, Matrix.single, Star.star
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : DecidableEq m
inst_2 : AddMonoid α
inst_3 : StarAddMonoid α
i : m
j : n
a : α
⊢ (single i j a)ᵀ.map (⇑starAddEquiv : (a : α) → α) = single j i (star a)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
v : n → α
rw : (diagonal fun (m : n) ↦ star (v m)) = diagonal (star v)
⊢ (diagonal v)ᴴ = diagonal (star v)

Tactic:
rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]

Premises used: Matrix.diagonal_transpose, star_zero, Matrix.diagonal_map, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
v : n → α
⊢ (diagonal fun (m : n) ↦ star (v m)) = diagonal (star v)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
x : n → α
⊢ (diagonal x).map star = diagonal (star x)

Tactic:
diagonal_map (star_zero _)

Premises used: star_zero, Matrix.diagonal_map
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : Star α
A : Matrix n n α
⊢ Aᴴ.diag = star A.diag

Tactic:
rfl

Premises used: Matrix.diag, Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : Star α
A : Matrix n n α
⊢ (A.map star).diag = star A.diag

Tactic:
rfl

Premises used: Matrix.diag, Matrix.map, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalSemiring α
inst_2 : StarRing α
v w : m → α
⊢ star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalSemiring α
inst_2 : StarRing α
v w : m → α
⊢ star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalSemiring α
inst_2 : StarRing α
v w : m → α
⊢ v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : StarRing α
M : Matrix m n α
v : n → α
⊢ star (M *ᵥ v) = star v ᵥ* Mᴴ

Tactic:
funext fun _ => (star_dotProduct_star _ _).symm

Premises used: Matrix.star_dotProduct_star, funext, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
inst_2 : StarRing α
M : Matrix m n α
v : m → α
⊢ star (v ᵥ* M) = Mᴴ *ᵥ star v

Tactic:
funext fun _ => (star_dotProduct_star _ _).symm

Premises used: Matrix.star_dotProduct_star, funext, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype m
inst_2 : StarRing α
A : Matrix m n α
x : m → α
⊢ Aᴴ *ᵥ x = star (star x ᵥ* A)

Tactic:
funext fun _ => star_dotProduct _ _

Premises used: Matrix.star_dotProduct, funext, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : NonUnitalSemiring α
inst_1 : Fintype n
inst_2 : StarRing α
A : Matrix m n α
x : n → α
⊢ x ᵥ* Aᴴ = star (A *ᵥ star x)

Tactic:
funext fun _ => dotProduct_star _ _

Premises used: Matrix.dotProduct_star, funext, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v)ᴴ = vecMulVec (star v) (star w)

Tactic:
ext fun _ _ => star_mul _ _

Premises used: StarMul.star_mul, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : StarMul α
w : m → α
v : n → α
rw : (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ
⊢ (vecMulVec w v).map star = (vecMulVec (star v) (star w))ᵀ

Tactic:
rw [← conjTranspose_vecMulVec]

Premises used: Matrix.conjTranspose_vecMulVec
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Star α
M : Matrix m n α
i : m
j : n
⊢ Mᴴ j i = star (M i j)

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : InvolutiveStar α
M : Matrix m n α
⊢ ∀ (i : m) (j : n), Mᴴᴴ i j = M i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : InvolutiveStar α
⊢ Function.Involutive (α := Matrix n n α) conjTranspose

Tactic:
conjTranspose_conjTranspose

Premises used: Function.Involutive, Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Star α
M : Matrix m n α
⊢ Mᴴᵀ = M.map star

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Star α
M : Matrix m n α
⊢ Mᵀᴴ = M.map star

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : InvolutiveStar α
⊢ Function.Injective (α := Matrix m n α) conjTranspose

Tactic:
(map_injective star_injective).comp transpose_injective

Premises used: Matrix.map_injective, star_injective, Matrix.transpose_injective, Function.Injective.comp, Matrix.map, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : InvolutiveStar α
A B : Matrix m n α
⊢ Aᴴ = Bᴴ ↔ A = B

Tactic:
conjTranspose_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matrix.conjTranspose_injective
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : Matrix n n α
v : n → α
rw rw₁ : M = diagonal (star v) ↔ M = diagonal (star v)
⊢ M = (diagonal v)ᴴ ↔ M = diagonal (star v)

Tactic:
rw [diagonal_conjTranspose]

Premises used: Matrix.diagonal_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : Matrix n n α
v : n → α
rw rw₁ : M = diagonal (star v) ↔ M = diagonal (star v)
⊢ M = (diagonal v).map star ↔ M = diagonal (star v)

Tactic:
rw [map_diagonal_star]

Premises used: Matrix.map_diagonal_star
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
⊢ ∀ (i : n) (j : m), Eq.{v + 1} (α := α) (0ᴴ i j) (0 i j)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
M : Matrix m n α
rw : Mᴴ = 0 ↔ Mᴴ = 0ᴴ
rw₁ rw₂ : Mᴴ = 0 ↔ Mᴴ = 0
⊢ Mᴴ = 0 ↔ M = 0

Tactic:
rw [← conjTranspose_inj (A := M), conjTranspose_zero]

Premises used: Matrix.conjTranspose_zero, Matrix.conjTranspose_inj
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
M : Matrix m n α
⊢ M.map star = 0 ↔ M = 0

Tactic:
simp [← ext_iff]

Premises used: Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
⊢ Eq (α := Matrix n n α) 1ᴴ 1

Tactic:
simp [conjTranspose]

Premises used: Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
rw rw₁ : M = 1 ↔ M = 1
⊢ M = 1ᴴ ↔ M = 1

Tactic:
rw [conjTranspose_one]

Premises used: Matrix.conjTranspose_one
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
⊢ M = map 1 star ↔ M = 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
d : ℕ
⊢ Eq (α := Matrix n n α) (↑d : Matrix n n α)ᴴ (↑d : Matrix n n α)

Tactic:
simp [conjTranspose, Matrix.map_natCast, diagonal_natCast]

Premises used: Matrix.diagonal_natCast, Matrix.map_natCast, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
d : ℕ
⊢ Eq (α := Matrix n n α) (map (↑d : Matrix n n α) star) (↑d : Matrix n n α)

Tactic:
simp [Matrix.map_natCast, diagonal_natCast]

Premises used: Matrix.diagonal_natCast, Matrix.map_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
d : ℕ
rw rw₁ : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
⊢ M = (↑d : Matrix n n α)ᴴ ↔ M = (↑d : Matrix n n α)

Tactic:
rw [conjTranspose_natCast]

Premises used: Matrix.conjTranspose_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
d : ℕ
rw rw₁ : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
⊢ M = map (↑d : Matrix n n α) star ↔ M = (↑d : Matrix n n α)

Tactic:
rw [map_natCast_star]

Premises used: Matrix.map_natCast_star
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
d : ℕ
inst_3 : d.AtLeastTwo
⊢ Eq (α := Matrix n n α) (OfNat.ofNat d)ᴴ (OfNat.ofNat d)

Tactic:
conjTranspose_natCast _

Premises used: Matrix.conjTranspose_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
d : ℕ
inst_3 : d.AtLeastTwo
⊢ Eq (α := Matrix n n α) (map (OfNat.ofNat d) star) (OfNat.ofNat d)

Tactic:
map_natCast_star _

Premises used: Matrix.map_natCast_star
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Semiring α
inst_2 : StarRing α
M : Matrix n n α
d : ℕ
inst_3 : d.AtLeastTwo
⊢ Mᴴ = OfNat.ofNat d ↔ M = OfNat.ofNat d

Tactic:
conjTranspose_eq_natCast

Premises used: Matrix.conjTranspose_eq_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Semiring α
inst_2 : StarRing α
M : Matrix n n α
d : ℕ
inst_3 : d.AtLeastTwo
⊢ M.map star = OfNat.ofNat d ↔ M = OfNat.ofNat d

Tactic:
map_star_eq_natCast

Premises used: Matrix.map_star_eq_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Ring α
inst_2 : StarRing α
d : ℤ
⊢ Eq (α := Matrix n n α) (↑d : Matrix n n α)ᴴ (↑d : Matrix n n α)

Tactic:
simp [conjTranspose, Matrix.map_intCast, diagonal_intCast]

Premises used: Matrix.map_intCast, Matrix.conjTranspose, Matrix.diagonal_intCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Ring α
inst_2 : StarRing α
d : ℤ
⊢ Eq (α := Matrix n n α) (map (↑d : Matrix n n α) star) (↑d : Matrix n n α)

Tactic:
simp [Matrix.map_intCast, diagonal_intCast]

Premises used: Matrix.map_intCast, Matrix.diagonal_intCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Ring α
inst_2 : StarRing α
M : Matrix n n α
d : ℤ
rw rw₁ : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
⊢ M = (↑d : Matrix n n α)ᴴ ↔ M = (↑d : Matrix n n α)

Tactic:
rw [conjTranspose_intCast]

Premises used: Matrix.conjTranspose_intCast
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Ring α
inst_2 : StarRing α
M : Matrix n n α
d : ℤ
rw rw₁ : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
⊢ M = map (↑d : Matrix n n α) star ↔ M = (↑d : Matrix n n α)

Tactic:
rw [map_intCast_star]

Premises used: Matrix.map_intCast_star
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M + N)ᴴ i j = (Mᴴ + Nᴴ) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddGroup α
inst_1 : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M - N)ᴴ i j = (Mᴴ - Nᴴ) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Star R
inst_1 : Star α
inst_2 : SMul R α
inst_3 : StarModule R α
c : R
M : Matrix m n α
⊢ (c • M)ᴴ = star c • Mᴴ

Tactic:
Matrix.ext fun _ _ => star_smul _ _

Premises used: StarModule.star_smul, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Star R
inst_1 : Star α
inst_2 : SMul R α
inst_3 : SMul.{u_7, v} Rᵐᵒᵖ α
c : R
M : Matrix m n α
h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (MulOpposite.op (star c) • Mᴴ) i j

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : StarMul α
c : α
M : Matrix m n α
⊢ (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ

Tactic:
conjTranspose_smul_non_comm c M star_mul

Premises used: StarMul.star_mul, Matrix.conjTranspose_smul_non_comm
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
c : ℕ
M : Matrix m n α
⊢ (c • M)ᴴ = c • Mᴴ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddGroup α
inst_1 : StarAddMonoid α
c : ℤ
M : Matrix m n α
⊢ (c • M)ᴴ = c • Mᴴ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (HSMul.hSMul (α := R) (↑c : R) M)ᴴ i j = HSMul.hSMul (α := R) (↑c : R) Mᴴ i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℕ
inst_4 : c.AtLeastTwo
M : Matrix m n α
⊢ (HSMul.hSMul (α := R) (OfNat.ofNat c) M)ᴴ = HSMul.hSMul (α := R) (OfNat.ofNat c) Mᴴ

Tactic:
conjTranspose_natCast_smul c M

Premises used: Matrix.conjTranspose_natCast_smul
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : Ring R
inst_1 : AddCommGroup α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (HSMul.hSMul (α := R) (↑c : R) M)ᴴ i j = HSMul.hSMul (α := R) (↑c : R) Mᴴ i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : DivisionSemiring R
inst_1 : AddCommMonoid α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (HSMul.hSMul (α := R) (↑c : R)⁻¹ M)ᴴ i j = HSMul.hSMul (α := R) (↑c : R)⁻¹ Mᴴ i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : DivisionSemiring R
inst_1 : AddCommMonoid α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℕ
inst_4 : c.AtLeastTwo
M : Matrix m n α
⊢ (HSMul.hSMul (α := R) (OfNat.ofNat c)⁻¹ M)ᴴ = HSMul.hSMul (α := R) (OfNat.ofNat c)⁻¹ Mᴴ

Tactic:
conjTranspose_inv_natCast_smul c M

Premises used: Matrix.conjTranspose_inv_natCast_smul
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : DivisionRing R
inst_1 : AddCommGroup α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (HSMul.hSMul (α := R) (↑c : R)⁻¹ M)ᴴ i j = HSMul.hSMul (α := R) (↑c : R)⁻¹ Mᴴ i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : DivisionRing R
inst_1 : AddCommGroup α
inst_2 : StarAddMonoid α
inst_3 : Module R α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (HSMul.hSMul (α := R) (↑c : R) M)ᴴ i j = HSMul.hSMul (α := R) (↑c : R) Mᴴ i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddCommGroup α
inst_1 : StarAddMonoid α
inst_2 : Module ℚ α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j

Tactic:
simp