-- Mathlib/Data/Matrix/Basis.lean
theorem induction_on'
    [AddCommMonoid α] [Finite m] [Finite n] {P : Matrix m n α → Prop} (M : Matrix m n α)
    (h_zero : P 0) (h_add : ∀ p q, P p → P q → P (p + q))
    (h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)) : P M

Proof state:
case intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝ : Fintype m
⊢ P M

Tactic:
cases nonempty_fintype n

Result:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P M

Proof state:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (stdBasisMatrix x✝.1 x✝.2 (M x✝.1 x✝.2))

Tactic:
apply h_std_basis

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P M

Tactic:
cases nonempty_fintype m

Result:
case intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝ : Fintype m
⊢ P M

Proof state:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, stdBasisMatrix x.1 x.2 (M x.1 x.2))

Tactic:
apply Finset.sum_induction _ _ h_add h_zero

Result:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (stdBasisMatrix x.1 x.2 (M x.1 x.2))

Proof state:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P M

Tactic:
rw [matrix_eq_sum_stdBasisMatrix M, ← Finset.sum_product']

Result:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, stdBasisMatrix x.1 x.2 (M x.1 x.2))

Proof state:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (stdBasisMatrix x.1 x.2 (M x.1 x.2))

Tactic:
intros

Result:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
val✝¹ : Fintype m
val✝ : Fintype n
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (stdBasisMatrix x✝.1 x✝.2 (M x✝.1 x✝.2))