-- Mathlib/Data/Matrix/Basis.lean
theorem ext_addMonoidHom
    [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] ⦃f g : Matrix m n α →+ β⦄
    (h : ∀ i j, f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)) :
    f = g

Proof state:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ f = g

Tactic:
ext x

Result:
case intro.intro.h
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ f x = g x

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
⊢ f = g

Tactic:
cases nonempty_fintype m

Result:
case intro
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝ : Fintype m
⊢ f = g

Proof state:
case intro.intro.h
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ f x = g x

Tactic:
rw [matrix_eq_sum_stdBasisMatrix x]

Result:
case intro.intro.h
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ f (∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)) = g (∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j))

Proof state:
case intro.intro.h.a.a
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
x✝¹ : m
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ f (stdBasisMatrix x✝¹ x✝ (x x✝¹ x✝)) = g (stdBasisMatrix x✝¹ x✝ (x x✝¹ x✝))

Tactic:
exact DFunLike.congr_fun (h _ _) _

Result:
no goals

Proof state:
case intro.intro.h
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ ∑ x_1 : m, ∑ x_2 : n, f (stdBasisMatrix x_1 x_2 (x x_1 x_2)) =
    ∑ x_1 : m, ∑ x_2 : n, g (stdBasisMatrix x_1 x_2 (x x_1 x_2))

Tactic:
congr! 2

Result:
case intro.intro.h.a.a
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
x✝¹ : m
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ f (stdBasisMatrix x✝¹ x✝ (x x✝¹ x✝)) = g (stdBasisMatrix x✝¹ x✝ (x x✝¹ x✝))

Proof state:
case intro
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝ : Fintype m
⊢ f = g

Tactic:
cases nonempty_fintype n

Result:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ f = g

Proof state:
case intro.intro.h
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ f (∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)) = g (∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j))

Tactic:
simp_rw [map_sum]

Result:
case intro.intro.h
m : Type u_2
n : Type u_3
α : Type u_5
β : Type u_6
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ ∑ x_1 : m, ∑ x_2 : n, f (stdBasisMatrix x_1 x_2 (x x_1 x_2)) =
    ∑ x_1 : m, ∑ x_2 : n, g (stdBasisMatrix x_1 x_2 (x x_1 x_2))