[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : 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
⊢ map (map M f) g = map M fun i j x => g (f x)
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : 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
⊢ map (map M f) g i✝ j✝ = map M (fun i j x => g (f x)) i✝ j✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : ∀ (i : m) (j : n), Subsingleton (α i j)
⊢ Subsingleton (DMatrix m n α)
[PROOFSTEP]
constructor
[GOAL]
case allEq
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : ∀ (i : m) (j : n), Subsingleton (α i j)
⊢ ∀ (a b : DMatrix m n α), a = b
[PROOFSTEP]
simp only [DMatrix, eq_iff_true_of_subsingleton, implies_true]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
⊢ map 0 f = 0
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = OfNat.ofNat 0 i✝ j✝
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ (map (M + N) fun i j => ↑f) = (map M fun i j => ↑f) + map N fun i j => ↑f
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ map (M + N) (fun i j => ↑f) i✝ j✝ = ((map M fun i j => ↑f) + map N fun i j => ↑f) i✝ j✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ (map (M - N) fun i j => ↑f) = (map M fun i j => ↑f) - map N fun i j => ↑f
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ map (M - N) (fun i j => ↑f) i✝ j✝ = ((map M fun i j => ↑f) - map N fun i j => ↑f) i✝ j✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty m
M N : DMatrix m n α
⊢ M = N
[PROOFSTEP]
ext i
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty m
M N : DMatrix m n α
i : m
j✝ : n
⊢ M i j✝ = N i j✝
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
⊢ M = N
[PROOFSTEP]
ext i j
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j
[PROOFSTEP]
exact isEmptyElim j
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
⊢ (fun M => DMatrix.map M fun i j => ↑f) 0 = 0
[PROOFSTEP]
simp
