-- Mathlib/Data/Matrix/Composition.lean
theorem comp_diagonal_diagonal [DecidableEq I] [DecidableEq J] [Zero R] (d : I → J → R) :
    comp I I J J R (diagonal fun i => diagonal fun j => d i j)
      = diagonal fun ij => d ij.1 ij.2

Proof state:
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
⊢ (comp I I J J R) (diagonal fun i => diagonal fun j => d i j) = diagonal fun ij => d ij.1 ij.2

Tactic:
ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩

Result:
case a.mk.mk
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
⊢ (comp I I J J R) (diagonal fun i => diagonal fun j => d i j) (i₁, j₁) (i₂, j₂) =
    diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Proof state:
case a.mk.mk.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
hi : i₁ ≠ i₂
⊢ diagonal (fun i => diagonal fun j => d i j) i₁ i₂ j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Tactic:
rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
  Matrix.zero_apply]

Result:
no goals

Proof state:
case a.mk.mk.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun i => diagonal fun j => d i j) i₁ i₁ j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Tactic:
rw [diagonal_apply_eq]

Result:
case a.mk.mk.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun j => d i₁ j) j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Proof state:
case a.mk.mk.inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ diagonal (fun j => d i₁ j) j₁ j₁ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₁)

Tactic:
rw [diagonal_apply_eq, diagonal_apply_eq]

Result:
no goals

Proof state:
case a.mk.mk.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun j => d i₁ j) j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Tactic:
obtain hj | rfl := ne_or_eq j₁ j₂

Result:
case a.mk.mk.inr.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
hj : j₁ ≠ j₂
⊢ diagonal (fun j => d i₁ j) j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

case a.mk.mk.inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ diagonal (fun j => d i₁ j) j₁ j₁ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₁)

Proof state:
case a.mk.mk
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
⊢ (comp I I J J R) (diagonal fun i => diagonal fun j => d i j) (i₁, j₁) (i₂, j₂) =
    diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Tactic:
dsimp [comp_apply]

Result:
case a.mk.mk
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
⊢ diagonal (fun i => diagonal fun j => d i j) i₁ i₂ j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Proof state:
case a.mk.mk
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
⊢ diagonal (fun i => diagonal fun j => d i j) i₁ i₂ j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Tactic:
obtain hi | rfl := ne_or_eq i₁ i₂

Result:
case a.mk.mk.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
hi : i₁ ≠ i₂
⊢ diagonal (fun i => diagonal fun j => d i j) i₁ i₂ j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

case a.mk.mk.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun i => diagonal fun j => d i j) i₁ i₁ j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Proof state:
case a.mk.mk.inr.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
hj : j₁ ≠ j₂
⊢ diagonal (fun j => d i₁ j) j₁ j₂ = diagonal (fun ij => d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Tactic:
rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]

Result:
no goals