l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ submatrix (diagonal d) e e i j = diagonal (d ∘ e) i j
rw [submatrix_apply]
case pos
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

case neg
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
by_cases h : i = j
case pos
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = (d ∘ e) j
case pos
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
rw [h, diagonal_apply_eq, diagonal_apply_eq]
no goals
case pos
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = (d ∘ e) j
simp only [Function.comp_apply]
no goals
case neg
l : Type u_2
m : Type u_1
n : Type ?u.1089606
o : Type ?u.1089609
m' : o → Type ?u.1089614
n' : o → Type ?u.1089619
R : Type ?u.1089622
S : Type ?u.1089625
α : Type v
β : Type w
γ : Type ?u.1089632
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]