awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Nonempty n
r s : α
⊢ Eq (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α)
      ((scalar n : (a : α) → Matrix n n α) s : Matrix n n α) ↔
    r = s

Tactic:
(diagonal_injective.comp Function.const_injective).eq_iff

Premises used: Function.Injective.eq_iff, Function.const_injective, Matrix.diagonal_injective, Function.Injective.comp, Matrix.diagonal, ite
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : Fintype m
r : α
M : Matrix m n α
simp_rw :
  HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ r) M =
      HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ r) ↔
    r • M = MulOpposite.op r • M
simp_rw₁ : r • M = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ r) ↔ r • M = MulOpposite.op r • M
⊢ HMul.hMul (α := Matrix m m α) ((scalar m : (a : α) → Matrix m m α) r : Matrix m m α) M =
      HMul.hMul (β := Matrix n n α) M ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) ↔
    r • M = MulOpposite.op r • M

Tactic:
simp_rw [scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]

Premises used: Matrix.op_smul_eq_mul_diagonal, Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
r : α
M : Matrix n n α
⊢ Commute ((scalar n : (a : α) → Matrix n n α) r) M ↔ r • M = MulOpposite.op r • M

Tactic:
scalar_comm_iff

Premises used: SemiconjBy, Commute, Matrix.scalar_comm_iff
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : Fintype m
r : α
hr : ∀ (r' : α), Commute r r'
M : Matrix m n α
⊢ HMul.hMul (α := Matrix m m α) ((scalar m : (a : α) → Matrix m m α) r : Matrix m m α) M =
    HMul.hMul (β := Matrix n n α) M ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α)

Tactic:
scalar_comm_iff.2 <| ext fun _ _ => hr _

Premises used: Iff.mpr, Matrix.scalar_comm_iff, Matrix.ext
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
r : α
hr : ∀ (r' : α), Commute r r'
M : Matrix n n α
⊢ Commute ((scalar n : (a : α) → Matrix n n α) r) M

Tactic:
scalar_comm r hr M

Premises used: Matrix.scalar_comm, SemiconjBy, Commute
-- Module: Mathlib.Data.Matrix.Basic
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
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
r : R
x : Matrix n n α
a :
  ∀ (i j : n),
    (r • x) i j =
      HMul.hMul (α := Matrix n n α)
        ((RingHom.comp (scalar n) (algebraMap R α) : (a : R) → Matrix n n α) r : Matrix n n α) x i j
⊢ r • x =
    HMul.hMul (α := Matrix n n α) ((RingHom.comp (scalar n) (algebraMap R α) : (a : R) → Matrix n n α) r : Matrix n n α)
      x

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Basic
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
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
r : R
x : Matrix n n α
i j : n
⊢ (r • x) i j =
    HMul.hMul (α := Matrix n n α) ((RingHom.comp (scalar n) (algebraMap R α) : (a : R) → Matrix n n α) r : Matrix n n α)
      x i j

Tactic:
simp [Matrix.scalar, Algebra.smul_def r]

Premises used: Matrix.scalar, Algebra.smul_def
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Algebra R α
r : R
i j : n
⊢ Eq.{u_11 + 1} (α := α) ((algebraMap R (Matrix n n α) : (a : R) → Matrix n n α) r i j : α)
    (if i = j then (algebraMap R α : (a : R) → α) r else 0 : α)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Algebra R α
r : R
⊢ Eq (α := Matrix n n α) ((algebraMap R (Matrix n n α) : (a : R) → Matrix n n α) r : Matrix n n α)
    (diagonal ((algebraMap R (n → α) : (a : R) → n → α) r) : Matrix n n α)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Algebra R α
⊢ Eq (α := R →+* Matrix n n α) (algebraMap R (Matrix n n α)) (RingHom.comp (diagonalRingHom n α) (algebraMap R (n → α)))

Tactic:
rfl

Premises used: Matrix.scalar, Matrix.diagonalRingHom, Matrix.diagonal, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α : (a : R) → α) r) = (algebraMap R β : (a : R) → β) r
rw :
  Eq (α := Matrix n n β) (diagonal fun (m : n) ↦ f ((algebraMap R (n → α) : (a : R) → n → α) r m))
    (diagonal ((algebraMap R (n → β) : (a : R) → n → β) r))
⊢ Eq (α := Matrix n n β) (map ((algebraMap R (Matrix n n α) : (a : R) → Matrix n n α) r) f)
    ((algebraMap R (Matrix n n β) : (a : R) → Matrix n n β) r)

Tactic:
rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]

Premises used: Matrix.algebraMap_eq_diagonal, Matrix.diagonal_map
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α : (a : R) → α) r) = (algebraMap R β : (a : R) → β) r
⊢ Eq (α := Matrix n n β) (diagonal fun (m : n) ↦ f ((algebraMap R (n → α) : (a : R) → n → α) r m))
    (diagonal ((algebraMap R (n → β) : (a : R) → n → β) r))

Tactic:
simp [hf₂]
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Algebra R α
a : α
⊢ Eq (α := Matrix n n α) ((scalarAlgHom n R : (a : α) → Matrix n n α) a : Matrix n n α)
    ((scalar n : (a : α) → Matrix n n α) a : Matrix n n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Add α
i : m
j : n
⊢ Eq (α := Matrix m n α →ₙ+ α) (entryAddHom α i j)
    (AddHom.comp (AddHom.comp (Pi.evalAddHom (fun (x : n) ↦ α) j) (Pi.evalAddHom (fun (i : m) ↦ n → α) i))
      (↑(AddEquiv.symm ofAddEquiv) : Matrix m n α →ₙ+ m → n → α))

Tactic:
rfl

Premises used: Matrix.entryAddHom, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : AddZeroClass α
i : m
j : n
⊢ Eq (α := Matrix m n α →+ α) (entryAddMonoidHom α i j)
    (AddMonoidHom.comp
      (AddMonoidHom.comp (Pi.evalAddMonoidHom (fun (x : n) ↦ α) j) (Pi.evalAddMonoidHom (fun (i : m) ↦ n → α) i))
      (↑(AddEquiv.symm ofAddEquiv) : Matrix m n α →+ m → n → α))

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
inst : AddZeroClass α
i : m
⊢ Eq (α := Matrix m m α →+ α) (AddMonoidHom.comp (Pi.evalAddMonoidHom (fun (i : m) ↦ α) i) (diagAddMonoidHom m α))
    (entryAddMonoidHom α i i)

Tactic:
simp [AddMonoidHom.ext_iff]

Premises used: AddMonoidHom.ext_iff
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : AddZeroClass α
i : m
j : n
⊢ Eq (α := Matrix m n α →ₙ+ α) (↑(entryAddMonoidHom α i j) : Matrix m n α →ₙ+ α) (entryAddHom α i j)

Tactic:
rfl

Premises used: Matrix.entryAddHom, AddHomClass.toAddHom, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
i : m
j : n
⊢ Eq (α := Matrix m n α →ₗ[R] α) (entryLinearMap R α i j)
    (LinearMap.proj (φ := fun (a : n) ↦ α) j ∘ₗ
      LinearMap.proj (φ := fun (i : m) ↦ n → α) i ∘ₗ
        (↑(LinearEquiv.symm (ofLinearEquiv R)) : Matrix m n α →ₗ[R] m → n → α))

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
i : m
⊢ Eq (α := Matrix m m α →ₗ[R] α) (LinearMap.proj (φ := fun (i : m) ↦ α) i ∘ₗ diagLinearMap m R α)
    (entryLinearMap R α i i)

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
i : m
j : n
⊢ Eq (α := Matrix m n α →+ α) (↑(entryLinearMap R α i j) : Matrix m n α →+ α) (entryAddMonoidHom α i j)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl, Matrix.entryAddMonoidHom
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
i : m
j : n
⊢ Eq (α := Matrix m n α →ₙ+ α) (↑(entryLinearMap R α i j) : Matrix m n α →ₙ+ α) (entryAddHom α i j)

Tactic:
rfl

Premises used: Matrix.entryAddHom, AddHomClass.toAddHom, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
⊢ Eq (α := Matrix m n α ≃ Matrix m n α) (Equiv.refl α).mapMatrix (Equiv.refl (Matrix m n α))

Tactic:
rfl

Premises used: Equiv.mapMatrix, Matrix.map, Equiv.refl, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
f : α ≃ β
⊢ Eq (α := Matrix m n β ≃ Matrix m n α) (Equiv.symm f.mapMatrix) f.symm.mapMatrix

Tactic:
rfl

Premises used: Equiv.mapMatrix, Matrix.map, Equiv.symm, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
γ : Type u_13
f : α ≃ β
g : β ≃ γ
⊢ Eq (α := Matrix m n α ≃ Matrix m n γ) (Equiv.trans f.mapMatrix g.mapMatrix) (f.trans g).mapMatrix

Tactic:
rfl

Premises used: Equiv.trans, Equiv.mapMatrix, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : AddZeroClass α
⊢ Eq (α := Matrix m n α →+ Matrix m n α) (mapMatrix (id α)) (id (Matrix m n α))

Tactic:
rfl

Premises used: Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
γ : Type u_13
inst : AddZeroClass α
inst_1 : AddZeroClass β
inst_2 : AddZeroClass γ
f : β →+ γ
g : α →+ β
⊢ Eq (α := Matrix m n α →+ Matrix m n γ) (comp f.mapMatrix g.mapMatrix) (f.comp g).mapMatrix

Tactic:
rfl

Premises used: Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : AddZeroClass α
inst_1 : AddZeroClass β
f : α →+ β
i : m
j : n
⊢ comp (entryAddMonoidHom β i j) f.mapMatrix = f.comp (entryAddMonoidHom α i j)

Tactic:
rfl

Premises used: Matrix, Matrix.map, rfl, Matrix.entryAddMonoidHom
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : AddZeroClass α
inst_1 : AddZeroClass β
⊢ Eq (α := Matrix m n α →+ Matrix m n β) (mapMatrix 0) 0

Tactic:
rfl

Premises used: Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f g : α →+ β
⊢ (f + g).mapMatrix = HAdd.hAdd (α := Matrix m n α →+ Matrix m n β) f.mapMatrix g.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : AddZeroClass α
inst_1 : AddCommGroup β
f g : α →+ β
⊢ (f - g).mapMatrix = HSub.hSub (α := Matrix m n α →+ Matrix m n β) f.mapMatrix g.mapMatrix

Tactic:
rfl

Premises used: AddMonoidHom.mk', Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : AddZeroClass α
inst_1 : AddCommGroup β
f : α →+ β
⊢ Eq (α := Matrix m n α →+ Matrix m n β) (-f).mapMatrix (-f.mapMatrix)

Tactic:
rfl

Premises used: AddMonoidHom.mk', Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
A : Type u_10
α : Type u_11
β : Type u_12
inst : Monoid A
inst_1 : AddZeroClass α
inst_2 : AddMonoid β
inst_3 : DistribMulAction A β
a : A
f : α →+ β
⊢ (a • f).mapMatrix = HSMul.hSMul (β := Matrix m n α →+ Matrix m n β) a f.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, AddMonoidHom.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Add α
⊢ Eq (α := Matrix m n α ≃+ Matrix m n α) (mapMatrix (refl α)) (refl (Matrix m n α))

Tactic:
rfl

Premises used: AddEquiv.refl, Matrix.map, Equiv.refl, AddEquiv.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : Add α
inst_1 : Add β
f : α ≃+ β
⊢ Eq (α := Matrix m n β ≃+ Matrix m n α) (symm f.mapMatrix) f.symm.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, Equiv.symm, AddEquiv.mapMatrix, rfl, AddEquiv.symm
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Add α
inst_1 : Add β
inst_2 : Add γ
f : α ≃+ β
g : β ≃+ γ
⊢ Eq (α := Matrix m n α ≃+ Matrix m n γ) (trans f.mapMatrix g.mapMatrix) (f.trans g).mapMatrix

Tactic:
rfl

Premises used: Equiv.trans, AddEquiv.trans, Matrix.map, AddEquiv.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : Add α
inst_1 : Add β
f : α ≃+ β
i : m
j : n
⊢ Eq (α := Matrix m n α →ₙ+ β) (AddHom.comp (entryAddHom β i j) (↑f.mapMatrix : Matrix m n α →ₙ+ Matrix m n β))
    (AddHom.comp (↑f : α →ₙ+ β) (entryAddHom α i j))

Tactic:
rfl

Premises used: Matrix, Matrix.entryAddHom, AddHomClass.toAddHom, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
⊢ Eq (α := Matrix m n α →ₗ[R] Matrix m n α) (mapMatrix id) id

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
T : Type u_9
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
σᵣₛ : R →+* S
σₛₜ : S →+* T
σᵣₜ : R →+* T
inst_3 : RingHomCompTriple σᵣₛ σₛₜ σᵣₜ
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module S β
inst_9 : Module T γ
f : β →ₛₗ[σₛₜ] γ
g : α →ₛₗ[σᵣₛ] β
⊢ Eq (α := Matrix m n α →ₛₗ[σᵣₜ] Matrix m n γ) (f.mapMatrix ∘ₛₗ g.mapMatrix) (f ∘ₛₗ g).mapMatrix

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
σᵣₛ : R →+* S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
f : α →ₛₗ[σᵣₛ] β
i : m
j : n
⊢ entryLinearMap S β i j ∘ₛₗ f.mapMatrix = f ∘ₛₗ entryLinearMap R α i j

Tactic:
rfl

Premises used: Matrix.entryLinearMap, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
σᵣₛ : R →+* S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
⊢ Eq (α := Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) (mapMatrix 0) 0

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
σᵣₛ : R →+* S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
f g : α →ₛₗ[σᵣₛ] β
⊢ (f + g).mapMatrix = HAdd.hAdd (α := Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) f.mapMatrix g.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
A : Type u_10
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
σᵣₛ : R →+* S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
inst_6 : Monoid A
inst_7 : DistribMulAction A β
inst_8 : SMulCommClass S A β
a : A
f : α →ₛₗ[σᵣₛ] β
⊢ (a • f).mapMatrix = HSMul.hSMul (β := Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) a f.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
σᵣₛ : R →+* S
inst_2 : AddCommMonoid α
inst_3 : AddCommGroup β
inst_4 : Module R α
inst_5 : Module S β
f g : α →ₛₗ[σᵣₛ] β
⊢ (f - g).mapMatrix = HSub.hSub (α := Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) f.mapMatrix g.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
σᵣₛ : R →+* S
inst_2 : AddCommMonoid α
inst_3 : AddCommGroup β
inst_4 : Module R α
inst_5 : Module S β
f : α →ₛₗ[σᵣₛ] β
⊢ Eq (α := Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) (-f).mapMatrix (-f.mapMatrix)

Tactic:
rfl

Premises used: Matrix.map, LinearMap.mapMatrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
⊢ Eq (α := Matrix m n α ≃ₗ[R] Matrix m n α) (mapMatrix (refl R α)) (refl R (Matrix m n α))

Tactic:
rfl

Premises used: LinearEquiv.mapMatrix, Matrix.map, LinearEquiv.refl, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
σᵣₛ : R →+* S
σₛᵣ : S →+* R
inst_6 : RingHomInvPair σᵣₛ σₛᵣ
inst_7 : RingHomInvPair σₛᵣ σᵣₛ
f : α ≃ₛₗ[σᵣₛ] β
⊢ Eq (α := Matrix m n β ≃ₛₗ[σₛᵣ] Matrix m n α) (symm f.mapMatrix) f.symm.mapMatrix

Tactic:
rfl

Premises used: LinearEquiv.mapMatrix, LinearEquiv.symm, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
T : Type u_9
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : AddCommMonoid γ
inst_6 : Module R α
inst_7 : Module S β
inst_8 : Module T γ
σᵣₛ : R →+* S
σₛₜ : S →+* T
σᵣₜ : R →+* T
inst_9 : RingHomCompTriple σᵣₛ σₛₜ σᵣₜ
σₛᵣ : S →+* R
σₜₛ : T →+* S
σₜᵣ : T →+* R
inst_10 : RingHomCompTriple σₜₛ σₛᵣ σₜᵣ
inst_11 : RingHomInvPair σᵣₛ σₛᵣ
inst_12 : RingHomInvPair σₛᵣ σᵣₛ
inst_13 : RingHomInvPair σₛₜ σₜₛ
inst_14 : RingHomInvPair σₜₛ σₛₜ
inst_15 : RingHomInvPair σᵣₜ σₜᵣ
inst_16 : RingHomInvPair σₜᵣ σᵣₜ
f : α ≃ₛₗ[σᵣₛ] β
g : β ≃ₛₗ[σₛₜ] γ
⊢ Eq (α := Matrix m n α ≃ₛₗ[σᵣₜ] Matrix m n γ) (trans f.mapMatrix g.mapMatrix) (mapMatrix (f.trans g))

Tactic:
rfl

Premises used: LinearEquiv.mapMatrix, Matrix.map, LinearEquiv.trans, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
σᵣₛ : R →+* S
σₛᵣ : S →+* R
inst_6 : RingHomInvPair σᵣₛ σₛᵣ
inst_7 : RingHomInvPair σₛᵣ σᵣₛ
f : α ≃ₛₗ[σᵣₛ] β
⊢ Eq (α := Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) (↑f.mapMatrix : Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β)
    (↑f : α →ₛₗ[σᵣₛ] β).mapMatrix

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module S β
σᵣₛ : R →+* S
σₛᵣ : S →+* R
inst_6 : RingHomInvPair σᵣₛ σₛᵣ
inst_7 : RingHomInvPair σₛᵣ σᵣₛ
f : α ≃ₛₗ[σᵣₛ] β
i : m
j : n
⊢ entryLinearMap S β i j ∘ₛₗ (↑f.mapMatrix : Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β) =
    (↑f : α →ₛₗ[σᵣₛ] β) ∘ₛₗ entryLinearMap R α i j

Tactic:
simp only [mapMatrix_toLinearMap, LinearMap.entryLinearMap_comp_mapMatrix]

Premises used: LinearMap.entryLinearMap_comp_mapMatrix, LinearEquiv.mapMatrix_toLinearMap
-- Module: Mathlib.Data.Matrix.Basic
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
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
f : α →+* β
⊢ Eq (α := Matrix m m β) (map.{u_11, u_12, u_2, u_2} (α := α) 1 (⇑f : (a : α) → β)) 1

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
⊢ Eq (α := Matrix m m α →+* Matrix m m α) (mapMatrix (id α)) (id (Matrix m m α))

Tactic:
rfl

Premises used: RingHom.mapMatrix, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
f : β →+* γ
g : α →+* β
⊢ Eq (α := Matrix m m α →+* Matrix m m γ) (comp f.mapMatrix g.mapMatrix) (f.comp g).mapMatrix

Tactic:
rfl

Premises used: RingHom.mapMatrix, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
inst : Fintype m
inst_1 : DecidableEq m
α : Type u_14
β : Type u_15
inst_2 : Semiring α
inst_3 : Semiring β
M : Matrix m m α
f : α →+* β
a : ℕ
⊢ (M ^ a).map (⇑f : (a : α) → β) = HPow.hPow (α := Matrix m m β) (M.map (⇑f : (a : α) → β)) a

Tactic:
f.mapMatrix.map_pow M a

Premises used: Matrix.map, RingHom.map_pow
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
⊢ Eq (α := Matrix m m α ≃+* Matrix m m α) (mapMatrix (refl α)) (refl (Matrix m m α))

Tactic:
rfl

Premises used: RingEquiv.refl, Matrix.map, RingEquiv.mapMatrix, Equiv.refl, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
β : Type u_12
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
inst_3 : NonAssocSemiring β
f : α ≃+* β
⊢ Eq (α := Matrix m m β ≃+* Matrix m m α) (RingEquiv.symm f.mapMatrix) f.symm.mapMatrix

Tactic:
rfl

Premises used: Matrix.map, RingEquiv.mapMatrix, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
f : α ≃+* β
g : β ≃+* γ
⊢ Eq (α := Matrix m m α ≃+* Matrix m m γ) (RingEquiv.trans f.mapMatrix g.mapMatrix) (f.trans g).mapMatrix

Tactic:
rfl

Premises used: Equiv.trans, Matrix.map, RingEquiv.mapMatrix, RingEquiv.trans, rfl
-- Module: Mathlib.Data.Matrix.Basic
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
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α_1
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
α : Type u_14
inst_5 : Mul α
inst_6 : AddCommMonoid α
x : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ
⊢ (fun (M : (Matrix m m α)ᵐᵒᵖ) ↦ (unop M)ᵀ.map op) ((fun (M : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ) ↦ op (Mᵀ.map unop)) x) =
    x

Tactic:
aesop