case a.h
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ 1ᵀ i j = OfNat.ofNat 1 i j
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ 1ᵀ = 1
ext i j
case a.h
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
case a.h
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ 1ᵀ i j = OfNat.ofNat 1 i j
rw [transpose_apply, ← diagonal_one]
case pos
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
h : i = j
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j

case neg
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
h : ¬i = j
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
case a.h
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
by_cases i = j
no goals
case pos
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
h : i = j
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
simp only [h, diagonal_apply_eq]
no goals
case neg
l : Type ?u.924222
m : Type ?u.924225
n : Type u_1
o : Type ?u.924231
m' : o → Type ?u.924236
n' : o → Type ?u.924241
R : Type ?u.924244
S : Type ?u.924247
α : Type v
β : Type w
γ : Type ?u.924254
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
h : ¬i = j
⊢ diagonal (fun x => 1) j i = diagonal (fun x => 1) i j
simp only [diagonal_apply_ne _ h, diagonal_apply_ne' _ h]