awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
i j : n
d : ℕ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
rw₂ : Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ (↑d : α)) i j) (if i = j then (↑d : α) else 0)
rw₃ rw₄ : Eq.{v + 1} (α := α) (if i = j then (↑d : α) else 0) (if i = j then (↑d : α) else 0)
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)

Tactic:
rw [Nat.cast_ite, Nat.cast_zero, ← diagonal_natCast, diagonal_apply]

Premises used: Matrix.diagonal_natCast, Matrix.diagonal_apply, Nat.cast_ite, Nat.cast_zero
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
i j : n
d : ℕ
inst_2 : d.AtLeastTwo
⊢ Eq.{v + 1} (α := α) ((OfNat.ofNat d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)

Tactic:
natCast_apply

Premises used: Matrix.natCast_apply
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : AddGroupWithOne α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : ℤ
⊢ Eq (α := Matrix n n β) (map (↑d : Matrix n n α) f) (diagonal fun (x : n) ↦ f (↑d : α))

Tactic:
diagonal_map h

Premises used: Matrix.diagonal_map
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
d : ℤ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
rw₂ : Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ (↑d : α)) i j) (if i = j then (↑d : α) else 0)
rw₃ rw₄ : Eq.{v + 1} (α := α) (if i = j then (↑d : α) else 0) (if i = j then (↑d : α) else 0)
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)

Tactic:
rw [Int.cast_ite, Int.cast_zero, ← diagonal_intCast, diagonal_apply]

Premises used: Int.cast_zero, Matrix.diagonal_apply, Int.cast_ite, Matrix.diagonal_intCast
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
a : ∀ (i j : m), diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j
⊢ diagonal d = (of : (a : m → m → α) → Matrix m m α) fun (x x_1 : m) ↦ d default

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
i j : m
a : diagonal d default j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default j
a₁ : diagonal d default default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
a₂ : d default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
a₃ a₄ : d default = d default
⊢ diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j

Tactic:
rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]

Premises used: Inhabited.default, Matrix.diagonal_apply_eq, Matrix.of_apply, Subsingleton.elim
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
i : n
h : ∀ (x : n), (diagonal d).col i x = Pi.single (M := fun (j : n) ↦ α) i (d i) x
⊢ (diagonal d).col i = Pi.single (M := fun (j : n) ↦ α) i (d i)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
i x : n
⊢ (diagonal d).col i x = Pi.single (M := fun (j : n) ↦ α) i (d i) x

Tactic:
simp +contextual [diagonal, Pi.single_apply]

Premises used: Pi.single_apply, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
j : n
h : ∀ (x : n), (diagonal d).row j x = Pi.single (M := fun (j : n) ↦ α) j (d j) x
⊢ (diagonal d).row j = Pi.single (M := fun (j : n) ↦ α) j (d j)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
j x : n
⊢ (diagonal d).row j x = Pi.single (M := fun (j : n) ↦ α) j (d j) x

Tactic:
simp +contextual [diagonal, eq_comm, Pi.single_apply]

Premises used: Pi.single_apply, eq_comm, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ Eq (α := Matrix n n α) (diagonal 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
d : n → α
⊢ diagonal d = 1 ↔ d = 1

Tactic:
diagonal_injective.eq_iff' diagonal_one

Premises used: Function.Injective.eq_iff', Matrix.diagonal_injective, Matrix.diagonal_one
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
i j : n
⊢ Eq.{v + 1} (α := α) (1 i j) (if i = j then 1 else 0)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
i : n
⊢ Eq.{v + 1} (α := α) (1 i i) 1

Tactic:
diagonal_apply_eq _ i

Premises used: Matrix.diagonal_apply_eq
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
i j : n
⊢ i ≠ j → Eq.{v + 1} (α := α) (1 i j) 0

Tactic:
diagonal_apply_ne _

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
i j : n
⊢ j ≠ i → Eq.{v + 1} (α := α) (1 i j) 0

Tactic:
diagonal_apply_ne' _

Premises used: Matrix.diagonal_apply_ne'
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
a : ∀ (i j : n), map 1 f i j = 1 i j
⊢ Eq (α := Matrix n n β) (map 1 f) 1

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
a : f (if i = j then 1 else 0) = if i = j then 1 else 0
⊢ map 1 f i j = 1 i j

Tactic:
simp only [one_apply, map_apply]

Premises used: Matrix.one_apply, Matrix.map_apply
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
pos : i = j → f 1 = 1
neg : ¬i = j → f 0 = 0
⊢ f (if i = j then 1 else 0) = if i = j then 1 else 0

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
h : i = j
⊢ f 1 = 1

Tactic:
simp [h₀, h₁]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
h : ¬i = j
⊢ f 0 = 0

Tactic:
simp [h₀, h₁]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
i j : n
⊢ Eq.{v + 1} (α := α) (1 i j : α) (Pi.single (M := fun (x : n) ↦ α) i 1 j : α)

Tactic:
simp only [one_apply, Pi.single_apply, eq_comm]

Premises used: Matrix.one_apply, Pi.single_apply, eq_comm
-- Module: Mathlib.Data.Matrix.Diagonal
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 : DecidableEq n
inst_1 : AddMonoidWithOne α
rw : Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ 0) 0
rw₁ rw₂ : Eq (α := Matrix n n α) 0 0
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ (↑0 : α)) 0

Tactic:
rw [Nat.cast_zero, diagonal_zero]

Premises used: Matrix.diagonal_zero, Nat.cast_zero
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
n_1 : 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 : DecidableEq n_1
inst_1 : AddMonoidWithOne α
n : ℕ
rw :
  (diagonal fun (x : n_1) ↦ HAdd.hAdd (α := α) (↑n : α) 1) =
    HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
rw₁ :
  HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) (diagonal fun (x : n_1) ↦ 1) =
    HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
rw₂ rw₃ :
  HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1 =
    HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
⊢ (diagonal fun (x : n_1) ↦ (↑(n + 1) : α)) = HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1

Tactic:
rw [Nat.cast_succ, ← diagonal_add, diagonal_one]

Premises used: Nat.cast_succ, Matrix.diagonal_one, Matrix.diagonal_add
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
n_1 : 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 : DecidableEq n_1
inst_1 : AddGroupWithOne α
n : ℕ
rw rw₁ : Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) (diagonal fun (x : n_1) ↦ (↑n : α))
⊢ Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑(↑n : ℤ) : α)) (diagonal fun (x : n_1) ↦ (↑n : α))

Tactic:
rw [Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
n_1 : 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 : DecidableEq n_1
inst_1 : AddGroupWithOne α
n : ℕ
rw : Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ -(↑(n + 1) : α)) (-diagonal fun (x : n_1) ↦ (↑(n + 1) : α))
rw₁ rw₂ :
  Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ -(↑(n + 1) : α)) (diagonal fun (i : n_1) ↦ -(↑(n + 1) : α))
⊢ Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑(Int.negSucc n) : α))
    (-diagonal fun (x : n_1) ↦ (↑(n + 1) : α))

Tactic:
rw [Int.cast_negSucc, diagonal_neg]

Premises used: Int.cast_negSucc, Matrix.diagonal_neg
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
A : Matrix n n α
i : n
⊢ A.diag i = A i i

Tactic:
rfl

Premises used: Matrix.diag, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
a : n → α
⊢ (diagonal a).diag = a

Tactic:
funext <| @diagonal_apply_eq _ _ _ _ a

Premises used: Matrix.diagonal_apply_eq, funext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
A : Matrix n n α
⊢ Aᵀ.diag = A.diag

Tactic:
rfl

Premises used: Matrix.diag, Matrix.transpose, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : Zero α
⊢ Eq (α := (i : n) → α) (diag 0) 0

Tactic:
rfl

Premises used: Matrix.diag, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : Add α
A B : Matrix n n α
⊢ (A + B).diag = A.diag + B.diag

Tactic:
rfl

Premises used: Matrix.diag, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : Sub α
A B : Matrix n n α
⊢ (A - B).diag = A.diag - B.diag

Tactic:
rfl

Premises used: Matrix.diag, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : Neg α
A : Matrix n n α
⊢ (-A).diag = -A.diag

Tactic:
rfl

Premises used: Matrix.diag, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : SMul R α
r : R
A : Matrix n n α
⊢ (r • A).diag = r • A.diag

Tactic:
rfl

Premises used: Matrix.diag, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ Eq (α := (i : n) → α) (diag 1) 1

Tactic:
diag_diagonal _

Premises used: Matrix.diag, Matrix.diag_diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
f : α → β
A : Matrix n n α
⊢ (A.map f).diag = f ∘ A.diag

Tactic:
rfl

Premises used: Matrix.diag, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
M : Matrix n n α
v : n → α
rw rw₁ : M = diagonal v ↔ M = diagonal v
⊢ M = (diagonal v)ᵀ ↔ M = diagonal v

Tactic:
rw [diagonal_transpose]

Premises used: Matrix.diagonal_transpose
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ Eq (α := Matrix n n α) 1ᵀ 1

Tactic:
diagonal_transpose _

Premises used: Matrix.diagonal_transpose
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
M : Matrix n n α
⊢ Mᵀ = 1 ↔ M = 1

Tactic:
transpose_eq_diagonal

Premises used: Matrix.transpose_eq_diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
M : Matrix n n α
d : ℕ
⊢ Mᵀ = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)

Tactic:
transpose_eq_diagonal

Premises used: Matrix.transpose_eq_diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
d : ℕ
inst_2 : d.AtLeastTwo
⊢ Eq (α := Matrix n n α) (OfNat.ofNat d)ᵀ (OfNat.ofNat d)

Tactic:
transpose_natCast _

Premises used: Matrix.transpose_natCast
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
M : Matrix n n α
d : ℕ
inst_2 : d.AtLeastTwo
⊢ Mᵀ = OfNat.ofNat d ↔ M = OfNat.ofNat d

Tactic:
transpose_eq_diagonal

Premises used: Matrix.transpose_eq_diagonal, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
d : ℤ
⊢ Eq (α := Matrix n n α) (↑d : Matrix n n α)ᵀ (↑d : Matrix n n α)

Tactic:
diagonal_transpose _

Premises used: Matrix.diagonal_transpose
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
M : Matrix n n α
d : ℤ
⊢ Mᵀ = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)

Tactic:
transpose_eq_diagonal

Premises used: Matrix.transpose_eq_diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
rw : diagonal d (e i) (e j) = diagonal (d ∘ e) i j
⊢ (diagonal d).submatrix e e i j = diagonal (d ∘ e) i j

Tactic:
rw [submatrix_apply]

Premises used: Matrix.submatrix_apply
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
pos : ∀ (h : i = j), diagonal d (e i) (e j) = diagonal (d ∘ e) i j
neg : ∀ (h : ¬i = j), diagonal d (e i) (e j) = diagonal (d ∘ e) i j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
pos : diagonal d (e j) (e j) = diagonal (d ∘ e) j j
pos₁ : d (e j) = diagonal (d ∘ e) j j
pos₂ : d (e j) = (d ∘ e) j
pos₃ pos₄ : d (e j) = d (e j)
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]

Premises used: Matrix.diagonal_apply_eq, Function.comp_apply
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
neg : diagonal d (e i) (e j) = 0
neg₁ neg₂ : Eq.{v + 1} (α := α) 0 0
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]

Premises used: Function.Injective.ne, Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq m
inst_3 : DecidableEq l
e : l → m
he : Function.Injective e
⊢ Eq (α := Matrix l l α) (submatrix 1 e e) 1

Tactic:
submatrix_diagonal _ e he

Premises used: Matrix.submatrix_diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
A : Matrix m m α
e : l → m
⊢ (A.submatrix e e).diag = A.diag ∘ e

Tactic:
rfl

Premises used: Matrix.diag, Matrix.submatrix, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l ↪ m
⊢ Eq (α := Matrix l l α) ((diagonal d).submatrix (⇑e : (a : l) → m) (⇑e : (a : l) → m))
    (diagonal (d ∘ (⇑e : (a : l) → m)))

Tactic:
submatrix_diagonal d e e.injective

Premises used: Matrix.submatrix_diagonal, Function.Embedding.injective, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l ≃ m
⊢ Eq (α := Matrix l l α) ((diagonal d).submatrix (⇑e : (a : l) → m) (⇑e : (a : l) → m))
    (diagonal (d ∘ (⇑e : (a : l) → m)))

Tactic:
submatrix_diagonal d e e.injective

Premises used: Matrix.submatrix_diagonal, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq m
inst_3 : DecidableEq l
e : l ↪ m
⊢ Eq (α := Matrix l l α) (submatrix.{v, u_1, u_2, u_2, u_1} (m := m) (n := m) 1 (⇑e : (a : l) → m) (⇑e : (a : l) → m)) 1

Tactic:
submatrix_one e e.injective

Premises used: Matrix.submatrix_one, Function.Embedding.injective, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq m
inst_3 : DecidableEq l
e : l ≃ m
⊢ Eq (α := Matrix l l α) (submatrix.{v, u_1, u_2, u_2, u_1} (m := m) (n := m) 1 (⇑e : (a : l) → m) (⇑e : (a : l) → m)) 1

Tactic:
submatrix_one e e.injective

Premises used: Matrix.submatrix_one, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.Matrix.DualNumber
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
h1 :
  ∀ (i j : n),
    fst (M := Matrix n n R)
        ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
        i j =
      fst
        (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
          (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
            Matrix n n R × Matrix n n R)
          (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
            Matrix n n R × Matrix n n R))
        i j
h2 :
  ∀ (i j : n),
    snd (R := Matrix n n R)
        ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
        i j =
      snd
        (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
          (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
            Matrix n n R × Matrix n n R)
          (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
            Matrix n n R × Matrix n n R))
        i j
⊢ ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
      (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j)) =
    HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
      (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
        Matrix n n R × Matrix n n R)
      (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
        Matrix n n R × Matrix n n R)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.DualNumber
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
h1 : Eq (α := R) (fst (M := R) (∑ j_1 : n, A i j_1 * B j_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))
⊢ fst (M := Matrix n n R)
      ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
      i j =
    fst
      (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R × Matrix n n R)
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R × Matrix n n R))
      i j

Tactic:
dsimp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.DualNumber
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
h1 : Eq (α := R) (∑ i_1 : n, fst (A i i_1 * B i_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))
⊢ Eq (α := R) (fst (M := R) (∑ j_1 : n, A i j_1 * B j_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))

Tactic:
simp_rw [fst_sum]

Premises used: TrivSqZeroExt.fst_sum
-- Module: Mathlib.Data.Matrix.DualNumber
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
⊢ Eq (α := R) (∑ i_1 : n, fst (A i i_1 * B i_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))

Tactic:
rfl