awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : Fintype I
inst_2 : Fintype J
inst_3 : DecidableEq I
inst_4 : DecidableEq J
M : Matrix I I (Matrix J J R)
⊢ IsUnit (M := Matrix (I × J) (I × J) R)
      ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) M : Matrix (I × J) (I × J) R) ↔
    IsUnit M

Tactic:
isUnit_map_iff (compAlgEquiv _ _ _ ℕ) M

Premises used: isUnit_map_iff, Nat, Matrix.compAlgEquiv
-- Module: Mathlib.Data.Matrix.Composition
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : Fintype I
inst_2 : Fintype J
inst_3 : DecidableEq I
inst_4 : DecidableEq J
M : Matrix (I × J) (I × J) R
⊢ IsUnit (M := Matrix I I (Matrix J J R))
      (((comp I I J J R).symm : (a : Matrix (I × J) (I × J) R) → Matrix I I (Matrix J J R)) M :
        Matrix I I (Matrix J J R)) ↔
    IsUnit M

Tactic:
isUnit_map_iff (compAlgEquiv _ _ _ ℕ).symm M

Premises used: AlgEquiv.symm, isUnit_map_iff, Nat, Matrix.compAlgEquiv
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

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

Tactic:
ext_iff.mp

Premises used: Iff.mp, DMatrix.ext_iff
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
i : m
j : n
⊢ M.map (α := α) (β := β) f i j = f (M i j)

Tactic:
rfl

Premises used: DMatrix.map, rfl
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
a :
  ∀ (i : m) (j : n),
    (M.map (α := α) (β := β) f).map (α := β) (β := γ) g i j =
      M.map (α := α) (β := fun (x : m) (x_1 : n) ↦ γ x x_1) (fun (x : m) (x_1 : n) (x_2 : α x x_1) ↦ g (f x_2)) i j
⊢ (M.map (α := α) (β := β) f).map (α := β) (β := γ) g =
    M.map (α := α) (β := fun (x : m) (x_1 : n) ↦ γ x x_1) fun (x : m) (x_1 : n) (x_2 : α x x_1) ↦ g (f x_2)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i : m
j : n
⊢ (M.map (α := α) (β := β) f).map (α := β) (β := γ) g i j =
    M.map (α := α) (β := fun (x : m) (x_1 : n) ↦ γ x x_1) (fun (x : m) (x_1 : n) (x_2 : α x x_1) ↦ g (f x_2)) i j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : ∀ (i : m) (j : n), Subsingleton.{v + 1} (α i j)
⊢ Subsingleton (DMatrix m n α)

Tactic:
inferInstanceAs <| Subsingleton <| ∀ i j, α i j

Premises used: _private.0.DMatrix.instSubsingleton._proof_1
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → Zero (α i j)
i : m
j : n
⊢ Eq.{v + 1} (α := α i j) (0 i j) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → Neg (α i j)
M : DMatrix m n α
i : m
j : n
⊢ (-M) i j = -M i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → Add (α i j)
M N : DMatrix m n α
i : m
j : n
⊢ (M + N) i j = M i j + N i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → Sub (α i j)
M N : DMatrix m n α
i : m
j : n
⊢ (M - N) i j = M i j - N i j

Tactic:
rfl

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

Tactic:
ext
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), Eq (α := β i j) (f 0) 0
i : m
j : n
⊢ map (α := α) 0 (β := β) f i j = 0 i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M N : DMatrix m n α
a :
  ∀ (i : m) (j : n),
    (M + N).map (α := α) (β := β) (fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j =
      HAdd.hAdd (α := DMatrix m n β) (β := DMatrix m n β)
        (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
        (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j
⊢ ((M + N).map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) =
    HAdd.hAdd (α := DMatrix m n β) (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))

Tactic:
ext
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M N : DMatrix m n α
i : m
j : n
⊢ (M + N).map (α := α) (β := β) (fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j =
    HAdd.hAdd (α := DMatrix m n β) (β := DMatrix m n β)
      (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M N : DMatrix m n α
a :
  ∀ (i : m) (j : n),
    (M - N).map (α := α) (β := β) (fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j =
      HSub.hSub (α := DMatrix m n β) (β := DMatrix m n β)
        (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
        (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j
⊢ ((M - N).map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) =
    HSub.hSub (α := DMatrix m n β) (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))

Tactic:
ext
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M N : DMatrix m n α
i : m
j : n
⊢ (M - N).map (α := α) (β := β) (fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j =
    HSub.hSub (α := DMatrix m n β) (β := DMatrix m n β)
      (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j))
      (N.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) i j

Tactic:
simp
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty m
M N : DMatrix m n α
a : ∀ (i : m) (j : n), M i j = N i j
⊢ M = N

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty m
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
isEmptyElim i

Premises used: isEmptyElim
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty m
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
exact isEmptyElim i
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty n
M N : DMatrix m n α
a : ∀ (i : m) (j : n), M i j = N i j
⊢ M = N

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
isEmptyElim j

Premises used: isEmptyElim
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
exact isEmptyElim j
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
⊢ Eq (α := DMatrix m n β) (DMatrix.map (α := α) 0 (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j)) 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.DMatrix
Goal:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst_1 : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → AddMonoidHom.{v, w} (α i j) (β i j)
M : DMatrix m n α
⊢ Eq (α := DMatrix m n β) ((mapDMatrix (α := α) (β := β) f : (a : DMatrix m n α) → DMatrix m n β) M : DMatrix m n β)
    (M.map (α := α) (β := β) fun (i : m) (j : n) ↦ (⇑f : (a : α i j) → β i j) : DMatrix m n β)

Tactic:
rfl

Premises used: DMatrix.map, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
i j : n
⊢ diagonal d i j = if i = j then d i 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 α
d : n → α
i : n
⊢ diagonal d i i = d i

Tactic:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
i j : n
h : i ≠ j
⊢ diagonal d i j = 0

Tactic:
simp [diagonal, h]

Premises used: Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
i j : n
h : j ≠ i
⊢ diagonal d i j = 0

Tactic:
diagonal_apply_ne d h.symm

Premises used: Ne.symm, Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i

Tactic:
simpa using congr_arg (fun m : Matrix n n α => m i i) h

Premises used: congr_arg
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d₁ d₂ : n → α
h : ∀ (i : n), d₁ i = d₂ i
rw rw₁ : diagonal d₂ = diagonal d₂
⊢ diagonal d₁ = diagonal d₂

Tactic:
rw [show d₁ = d₂ from funext h]

Premises used: funext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i

Tactic:
simpa using Matrix.ext_iff.mpr h i i

Premises used: Iff.mpr, Matrix.ext_iff
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
a : ∀ (i j : n), Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ 0) i j) (0 i j)
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ 0) 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
i j : n
⊢ Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ 0) i j) (0 i j)

Tactic:
simp [diagonal]

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

Tactic:
diagonal_zero

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

Tactic:
diagonal_injective.eq_iff' diagonal_zero

Premises used: Matrix.diagonal_zero, Function.Injective.eq_iff', Matrix.diagonal_injective
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
a : ∀ (i j : n), (diagonal v)ᵀ i j = diagonal v i j
⊢ (diagonal v)ᵀ = diagonal v

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i j : n
pos : ∀ (h : i = j), (diagonal v)ᵀ i j = diagonal v i j
neg : ∀ (h : ¬i = j), (diagonal v)ᵀ i j = diagonal v i j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
simp [h, transpose, eqComm]

Premises used: Matrix.transpose, eqComm
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
simp [h, transpose, eqComm]

Premises used: Matrix.transpose, eqComm
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
a : ∀ (i j : n), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
⊢ diagonal d₁ + diagonal d₂ = diagonal fun (i : n) ↦ d₁ i + d₂ i

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
i j : n
pos : ∀ (h : i = j), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
neg : ∀ (h : ¬i = j), (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i + d₂ i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
a : ∀ (i j : n), diagonal (r • d) i j = (r • diagonal d) i j
⊢ diagonal (r • d) = r • diagonal d

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
i j : n
pos : ∀ (h : i = j), diagonal (r • d) i j = (r • diagonal d) i j
neg : ∀ (h : ¬i = j), diagonal (r • d) i j = (r • diagonal d) i j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
i j : n
h : i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
i j : n
h : ¬i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
a : ∀ (i j : n), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
⊢ -diagonal d = diagonal fun (i : n) ↦ -d i

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
i j : n
pos : ∀ (h : i = j), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
neg : ∀ (h : ¬i = j), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
⊢ (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
i j : n
h : i = j
⊢ (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
i j : n
h : ¬i = j
⊢ (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
a : ∀ (i j : n), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
⊢ diagonal d₁ - diagonal d₂ = diagonal fun (i : n) ↦ d₁ i - d₂ i

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
pos : ∀ (h : i = j), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
neg : ∀ (h : ¬i = j), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
simp : (∀ (i j : n), (if i = j then d i else 0) ∈ S) ↔ ∀ (i : n), d i ∈ S
⊢ Membership.mem (γ := Set (Matrix n n α)) S.matrix (diagonal d) ↔ ∀ (i : n), d i ∈ S

Tactic:
simp only [Set.mem_matrix, diagonal, of_apply]

Premises used: Set.mem_matrix, Matrix.of_apply, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i j : n
rw : (i = j → d i ∈ S) ∧ (¬i = j → 0 ∈ S)
| (if i = j then d i else 0) ∈ S

Tactic:
rw [ite_mem]

Premises used: ite_mem
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
conv_lhs : (∀ (i j : n), (i = j → d i ∈ S) ∧ (¬i = j → 0 ∈ S)) ↔ ∀ (i : n), d i ∈ S
⊢ (∀ (i j : n), (if i = j then d i else 0) ∈ S) ↔ ∀ (i : n), d i ∈ S

Tactic:
conv_lhs => intro _ _; rw [ite_mem]

Premises used: ite_mem
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ (∀ (i j : n), (i = j → d i ∈ S) ∧ (¬i = j → 0 ∈ S)) ↔ ∀ (i : n), d i ∈ S

Tactic:
simp [hS]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : NatCast α
m : ℕ
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ (↑m : α)) (↑m : Matrix n n α)

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 : NatCast α
m : ℕ
⊢ Eq (α := Matrix n n α) (diagonal (↑m : n → α)) (↑m : Matrix n n α)

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 : NatCast α
d : n → α
m : ℕ
⊢ diagonal d = (↑m : Matrix n n α) ↔ d = (↑m : n → α)

Tactic:
diagonal_injective.eq_iff' <| diagonal_natCast' _

Premises used: Matrix.diagonal_natCast', Function.Injective.eq_iff', Matrix.diagonal_injective
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : NatCast α
m : ℕ
inst_3 : m.AtLeastTwo
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ OfNat.ofNat m) (OfNat.ofNat m)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : NatCast α
m : ℕ
inst_3 : m.AtLeastTwo
⊢ Eq (α := Matrix n n α) (diagonal (OfNat.ofNat m)) (OfNat.ofNat m)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : NatCast α
d : n → α
m : ℕ
inst_3 : m.AtLeastTwo
⊢ diagonal d = OfNat.ofNat m ↔ d = OfNat.ofNat m

Tactic:
diagonal_injective.eq_iff' <| diagonal_ofNat' _

Premises used: Matrix.diagonal_ofNat', Function.Injective.eq_iff', Matrix.diagonal_injective
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : IntCast α
m : ℤ
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ (↑m : α)) (↑m : Matrix n n α)

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 : IntCast α
m : ℤ
⊢ Eq (α := Matrix n n α) (diagonal (↑m : n → α)) (↑m : Matrix n n α)

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 : IntCast α
d : n → α
m : ℤ
⊢ diagonal d = (↑m : Matrix n n α) ↔ d = (↑m : n → α)

Tactic:
diagonal_injective.eq_iff' <| diagonal_intCast' _

Premises used: Function.Injective.eq_iff', Matrix.diagonal_injective, Matrix.diagonal_intCast'
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
a : ∀ (i j : n), (diagonal d).map f i j = diagonal (fun (m : n) ↦ f (d m)) i j
⊢ (diagonal d).map f = diagonal fun (m : n) ↦ f (d m)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
a : f (if i = j then d i else 0) = if i = j then f (d i) else 0
⊢ (diagonal d).map f i j = diagonal (fun (m : n) ↦ f (d m)) i j

Tactic:
simp only [diagonal_apply, map_apply]

Premises used: Matrix.map_apply, Matrix.diagonal_apply
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
pos : i = j → f (d i) = f (d i)
neg : ¬i = j → f 0 = 0
⊢ f (if i = j then d i else 0) = if i = j then f (d i) 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 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
h_1 : i = j
⊢ f (d i) = f (d i)

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
h_1 : ¬i = j
⊢ f 0 = 0

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Diagonal
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
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
β : Type w
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : ℕ
inst_3 : d.AtLeastTwo
⊢ Eq (α := Matrix n n β) (map (OfNat.ofNat d) f) (diagonal fun (x : n) ↦ f (OfNat.ofNat d))

Tactic:
diagonal_map h

Premises used: Matrix.diagonal_map, Matrix.diagonal