awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : StarRing α
M : Matrix m n α
N : Matrix n l α
⊢ ∀ (i : l) (j : m), (M * N)ᴴ i j = (Nᴴ * Mᴴ) i j

Tactic:
simp [mul_apply]

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

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Star α
inst_1 : Star β
A : Matrix m n α
f : α → β
hf : Function.Semiconj f star star
⊢ Aᴴ.map f = (A.map f)ᴴ

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

Premises used: Matrix.transpose, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Star α
inst_1 : TrivialStar α
A : Matrix m n α
⊢ Aᴴ = Aᵀ

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

Premises used: TrivialStar.star_trivial, Matrix.transpose, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
⊢ Eq (α := Matrix n m α ≃+ Matrix m n α) (AddEquiv.symm (conjTransposeAddEquiv m n α)) (conjTransposeAddEquiv n m α)

Tactic:
rfl

Premises used: Matrix.map, Equiv.symm, Matrix.conjTranspose, Matrix.conjTransposeAddEquiv, rfl, AddEquiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
l : List (Matrix m n α)
⊢ l.sumᴴ = (List.map conjTranspose l).sum

Tactic:
map_list_sum (conjTransposeAddEquiv m n α) l

Premises used: map_list_sum, Matrix.map, Matrix.conjTranspose, Matrix.conjTransposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddCommMonoid α
inst_1 : StarAddMonoid α
s : Multiset (Matrix m n α)
⊢ s.sumᴴ = (Multiset.map conjTranspose s).sum

Tactic:
(conjTransposeAddEquiv m n α).toAddMonoidHom.map_multiset_sum s

Premises used: AddEquiv.toAddMonoidHom, Matrix.map, AddMonoidHom.map_multiset_sum, Matrix.conjTranspose, Matrix.conjTransposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddCommMonoid α
inst_1 : StarAddMonoid α
ι : Type u_10
s : Finset ι
M : ι → Matrix m n α
⊢ Eq (α := Matrix n m α) (∑ i ∈ s, M i)ᴴ (∑ i ∈ s, (M i)ᴴ)

Tactic:
map_sum (conjTransposeAddEquiv m n α) _ s

Premises used: map_sum, Matrix.map, Matrix.conjTranspose, Matrix.conjTransposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid α
inst_3 : StarAddMonoid α
inst_4 : Module R α
inst_5 : StarModule R α
⊢ Eq (α := Matrix n m α ≃ₗ⋆[R] Matrix m n α) (LinearEquiv.symm (conjTransposeLinearEquiv m n R α))
    (conjTransposeLinearEquiv n m R α)

Tactic:
rfl

Premises used: LinearEquiv.symm, Matrix.conjTransposeLinearEquiv, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
α : Type v
inst : Star α
M : Matrix m m α
⊢ star M = Mᴴ

Tactic:
rfl

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

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Star α
A : Matrix m n α
r : l → m
c : o → n
⊢ (A.submatrix r c)ᴴ = Aᴴ.submatrix c r

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Star α
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ Eq (α := Matrix o l α) ((reindex eₘ eₙ : (a : Matrix m n α) → Matrix l o α) M)ᴴ
    ((reindex eₙ eₘ : (a : Matrix n m α) → Matrix o l α) Mᴴ)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
α : Type v
inst : Semiring α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
M : Matrix m m α
k : ℕ
⊢ (M ^ k)ᴴ = Mᴴ ^ k

Tactic:
MulOpposite.op_injective <| map_pow (conjTransposeRingEquiv m α) M k

Premises used: MulOpposite.op_injective, map_pow, Matrix.conjTransposeRingEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
m : Type u_2
α : Type v
inst : Semiring α
inst_1 : StarRing α
inst_2 : Fintype m
inst_3 : DecidableEq m
l : List (Matrix m m α)
⊢ l.prodᴴ = (List.map conjTranspose l).reverse.prod

Tactic:
(conjTransposeRingEquiv m α).unop_map_list_prod l

Premises used: StarRingEquiv.toRingEquiv, Matrix.map, MulOpposite.unop, RingEquiv.unop_map_list_prod, Matrix.conjTranspose, Matrix.conjTransposeRingEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : StarRing R
inst_3 : TrivialStar R
inst_4 : Semiring α
inst_5 : StarRing α
inst_6 : Algebra R α
inst_7 : StarModule R α
r : R
M : Matrix n n α
change :
  (conjTransposeRingEquiv n α : (a : Matrix n n α) → (Matrix n n α)ᵐᵒᵖ) (r • M) =
    HSMul.hSMul (β := (Matrix n n α)ᵐᵒᵖ) r
      ((conjTransposeRingEquiv n α : (a : Matrix n n α) → (Matrix n n α)ᵐᵒᵖ) M : (Matrix n n α)ᵐᵒᵖ)
⊢ (RingEquiv.toEquiv (StarRingEquiv.toRingEquiv (conjTransposeRingEquiv n α))).toFun (r • M) =
    r • (RingEquiv.toEquiv (StarRingEquiv.toRingEquiv (conjTransposeRingEquiv n α))).toFun M

Tactic:
change conjTransposeRingEquiv n α (r • M) = r • conjTransposeRingEquiv n α M

Premises used: HSMul.hSMul, DFunLike.coe, Matrix.conjTransposeRingEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : StarRing R
inst_3 : TrivialStar R
inst_4 : Semiring α
inst_5 : StarRing α
inst_6 : Algebra R α
inst_7 : StarModule R α
r : R
M : Matrix n n α
⊢ (conjTransposeRingEquiv n α : (a : Matrix n n α) → (Matrix n n α)ᵐᵒᵖ) (r • M) =
    HSMul.hSMul (β := (Matrix n n α)ᵐᵒᵖ) r
      ((conjTransposeRingEquiv n α : (a : Matrix n n α) → (Matrix n n α)ᵐᵒᵖ) M : (Matrix n n α)ᵐᵒᵖ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M N : Matrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M N : Matrix m n α
⊢ (∀ (i : m) (j : n), M i j = N i j) → M = N

Tactic:
ext_iff.mp

Premises used: Iff.mp, Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
f : m → n → α
i : m
j : n
⊢ (of : (a : m → n → α) → Matrix m n α) f i j = f i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
f : Matrix m n α
i : m
j : n
⊢ (Equiv.symm of : (a : Matrix m n α) → m → n → α) f i j = f i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
f : α → β
i : m
j : n
⊢ M.map f i j = f (M i j)

Tactic:
rfl

Premises used: Matrix.map, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
a : ∀ (i : m) (j : n), M.map id i j = M i j
⊢ M.map id = M

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
⊢ M.map id i j = M i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ (M.map fun (x : α) ↦ x) = M

Tactic:
map_id M

Premises used: Matrix.map_id
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
a : ∀ (i : m) (j : n), (M.map f).map g i j = M.map (g ∘ f) i j
⊢ (M.map f).map g = M.map (g ∘ f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
i : m
j : n
⊢ (M.map f).map g i j = M.map (g ∘ f) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
f : α → β
hf : Function.Injective f
⊢ Function.Injective (β := Matrix m n β) fun (M : Matrix m n α) ↦ M.map f

Tactic:
fun _ _ h =>
  ext fun i j => hf <| ext_iff.mpr h i j

Premises used: Iff.mpr, Matrix.ext_iff, Function.Injective, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
f : α → α
hf : Function.Involutive f
x : Matrix m n α
⊢ (fun (M : Matrix m n α) ↦ M.map f) ((fun (M : Matrix m n α) ↦ M.map f) x) = x

Tactic:
simp [hf]
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : n
j : m
⊢ M.transpose i j = M j i

Tactic:
rfl

Premises used: Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : Subsingleton α
⊢ Subsingleton (Matrix m n α)

Tactic:
inferInstanceAs <| Subsingleton <| m → n → α

Premises used: _private.0.Matrix.subsingleton._proof_1
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : Nonempty m
inst_1 : Nonempty n
inst_2 : Nontrivial α
⊢ Nontrivial (Matrix m n α)

Tactic:
Function.nontrivial

Premises used: Function.nontrivial, Matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : SMul R α
inst_1 : SMul S α
inst_2 : SMulCommClass R S α
⊢ SMulCommClass R S (Matrix m n α)

Tactic:
Pi.smulCommClass

Premises used: Matrix, Pi.smulCommClass
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : SMul R S
inst_1 : SMul R α
inst_2 : SMul S α
inst_3 : IsScalarTower R S α
⊢ IsScalarTower R S (Matrix m n α)

Tactic:
Pi.isScalarTower

Premises used: Matrix, Pi.isScalarTower
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : SMul R α
inst_1 : SMul.{u_7, v} Rᵐᵒᵖ α
inst_2 : IsCentralScalar R α
⊢ IsCentralScalar R (Matrix m n α)

Tactic:
Pi.isCentralScalar

Premises used: Pi.isCentralScalar, Matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Zero α
i : m
j : n
⊢ Eq.{v + 1} (α := α) (0 i j) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
A B : Matrix m n α
i : m
j : n
⊢ (A + B) i j = A i j + B i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : SMul β α
r : β
A : Matrix m n α
i : m
j : n
⊢ (r • A) i j = r • A i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Sub α
A B : Matrix m n α
i : m
j : n
⊢ (A - B) i j = A i j - B i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Neg α
A : Matrix m n α
i : m
j : n
⊢ (-A) i j = -A i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
pos : ∀ (h : P), dite P A B i j = if x : P then A x i j else B x i j
neg : ∀ (h : ¬P), dite P A B i j = if x : P then A x i j else B x i j
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
by_cases h : P
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : P
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : ¬P
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst : Decidable P
A B : Matrix m n α
i : m
j : n
⊢ (if P then A else B) i j = if P then A i j else B i j

Tactic:
Matrix.dite_apply _ _ _ _ _

Premises used: Matrix.dite_apply, ite
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Zero α
⊢ Eq (α := Matrix m n α) ((of : (a : m → n → α) → Matrix m n α) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
f g : m → n → α
⊢ HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α) ((of : (a : m → n → α) → Matrix m n α) f : Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) g : Matrix m n α) =
    (of : (a : m → n → α) → Matrix m n α) (f + g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Sub α
f g : m → n → α
⊢ HSub.hSub (α := Matrix m n α) (β := Matrix m n α) ((of : (a : m → n → α) → Matrix m n α) f : Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) g : Matrix m n α) =
    (of : (a : m → n → α) → Matrix m n α) (f - g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Neg α
f : m → n → α
⊢ Eq (α := Matrix m n α) (-(of : (a : m → n → α) → Matrix m n α) f : Matrix m n α)
    ((of : (a : m → n → α) → Matrix m n α) (-f) : Matrix m n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst : SMul R α
r : R
f : m → n → α
⊢ HSMul.hSMul (β := Matrix m n α) r ((of : (a : m → n → α) → Matrix m n α) f : Matrix m n α) =
    (of : (a : m → n → α) → Matrix m n α) (r • f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Zero α
inst_1 : Zero β
f : α → β
h : f 0 = 0
a : ∀ (i : m) (j : n), map 0 f i j = 0 i j
⊢ Eq (α := Matrix m n β) (map 0 f) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Zero α
inst_1 : Zero β
f : α → β
h : f 0 = 0
i : m
j : n
⊢ map 0 f i j = 0 i j

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Add α
inst_1 : Add β
f : α → β
hf : ∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂
M N : Matrix m n α
⊢ (M + N).map f = M.map f + N.map f

Tactic:
ext fun _ _ => hf _ _

Premises used: Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Neg α
inst_1 : Neg β
f : α → β
hf : ∀ (a : α), f (-a) = -f a
M : Matrix m n α
⊢ (-M).map f = -M.map f

Tactic:
ext fun _ _ => hf _

Premises used: Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Sub α
inst_1 : Sub β
f : α → β
hf : ∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂
M N : Matrix m n α
⊢ (M - N).map f = M.map f - N.map f

Tactic:
ext fun _ _ => hf _ _

Premises used: Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst : SMul R α
inst_1 : SMul R β
f : α → β
r : R
hf : ∀ (a : α), f (r • a) = r • f a
M : Matrix m n α
⊢ (r • M).map f = r • M.map f

Tactic:
ext fun _ _ => hf _

Premises used: Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type v
β : Type w
inst : SMul R α
inst_1 : SMul S β
f : α → β
σ : R → S
r : R
hf : ∀ (a : α), f (r • a) = σ r • f a
M : Matrix m n α
⊢ (r • M).map f = σ r • M.map f

Tactic:
ext fun _ _ => hf _

Premises used: Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
n : Type u_3
α : Type v
β : Type w
inst : Mul α
inst_1 : Mul β
f : α → β
r : α
A : Matrix n n α
hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂
⊢ (r • A).map f = f r • A.map f

Tactic:
ext fun _ _ => hf _ _

Premises used: Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
n : Type u_3
α : Type v
β : Type w
inst : Mul α
inst_1 : Mul β
f : α → β
r : α
A : Matrix n n α
hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂
⊢ (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f

Tactic:
ext fun _ _ => hf _ _

Premises used: MulOpposite.unop, Matrix.ext, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst : SMul R S
k : R
hk : IsSMulRegular S k
⊢ IsSMulRegular (Matrix m n S) k

Tactic:
IsSMulRegular.pi fun _ => IsSMulRegular.pi fun _ => hk

Premises used: Matrix, IsSMulRegular.pi
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
k : α
hk : IsLeftRegular k
⊢ IsSMulRegular (Matrix m n α) k

Tactic:
hk.isSMulRegular.matrix

Premises used: IsLeftRegular.isSMulRegular, IsSMulRegular.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty m
M N : Matrix m n α
a : ∀ (i : m) (j : n), M i j = N i j
⊢ M = N

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty m
M N : Matrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
isEmptyElim i

Premises used: isEmptyElim
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty m
M N : Matrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
exact isEmptyElim i
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty n
M N : Matrix m n α
a : ∀ (i : m) (j : n), M i j = N i j
⊢ M = N

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty n
M N : Matrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
isEmptyElim j

Premises used: isEmptyElim
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty n
M N : Matrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
exact isEmptyElim j
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
⊢ Eq (α := (a : m → n → α) → Matrix m n α) (⇑ofAddEquiv : (a : m → n → α) → Matrix m n α)
    (⇑of : (a : m → n → α) → Matrix m n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
⊢ Eq (α := (a : Matrix m n α) → m → n → α) (⇑(AddEquiv.symm ofAddEquiv) : (a : Matrix m n α) → m → n → α)
    (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)

Tactic:
rfl

Premises used: Matrix.of, Equiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
A : Matrix m n α
simp_rw :
  (∃ (b : Matrix m n α), (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
    ∃ (f : (x : m) → (x : n) → α),
      (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0
⊢ IsAddUnit A ↔ ∀ (i : m) (j : n), IsAddUnit (A i j)

Tactic:
simp_rw [isAddUnit_iff_exists, Classical.skolem, forall_and,
    ← Matrix.ext_iff, add_apply, zero_apply]

Premises used: Classical.skolem, isAddUnit_iff_exists, Matrix.zero_apply, Matrix.add_apply, Matrix.ext_iff, forall_and
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
A : Matrix m n α
⊢ (∃ (b : Matrix m n α), (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
    ∃ (f : (x : m) → (x : n) → α),
      (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
a : ∀ (i : m) (j : n), Mᵀᵀ i j = M i j
⊢ Mᵀᵀ = M

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
⊢ Mᵀᵀ i j = M i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
n : Type u_3
α : Type v
⊢ Function.Involutive (α := Matrix n n α) transpose

Tactic:
transpose_transpose

Premises used: Matrix.transpose_transpose, Function.Involutive
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
⊢ Function.Injective (α := Matrix m n α) transpose

Tactic:
fun _ _ h => ext fun i j => ext_iff.2 h j i

Premises used: Iff.mpr, Matrix.ext_iff, Function.Injective, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A B : Matrix m n α
⊢ Aᵀ = Bᵀ ↔ A = B

Tactic:
transpose_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matrix.transpose_injective
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Zero α
⊢ Eq (α := Matrix n m α) 0ᵀ 0

Tactic:
rfl

Premises used: Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Zero α
M : Matrix m n α
⊢ Mᵀ = 0 ↔ M = 0

Tactic:
transpose_inj

Premises used: Matrix.transpose_inj, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
M N : Matrix m n α
a : ∀ (i : n) (j : m), (M + N)ᵀ i j = (Mᵀ + Nᵀ) i j
⊢ (M + N)ᵀ = Mᵀ + Nᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
M N : Matrix m n α
i : n
j : m
⊢ (M + N)ᵀ i j = (Mᵀ + Nᵀ) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Sub α
M N : Matrix m n α
a : ∀ (i : n) (j : m), (M - N)ᵀ i j = (Mᵀ - Nᵀ) i j
⊢ (M - N)ᵀ = Mᵀ - Nᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Sub α
M N : Matrix m n α
i : n
j : m
⊢ (M - N)ᵀ i j = (Mᵀ - Nᵀ) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
R : Type u_10
inst : SMul R α
c : R
M : Matrix m n α
⊢ (c • M)ᵀ = c • Mᵀ

Tactic:
rfl

Premises used: Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Neg α
M : Matrix m n α
⊢ (-M)ᵀ = -Mᵀ

Tactic:
rfl

Premises used: Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
f : α → β
M : Matrix m n α
⊢ Mᵀ.map f = (M.map f)ᵀ

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, rfl