-- Mathlib/Data/Matrix/Basis.lean
theorem mul_of_ne (i : l) (j k : m) {l : n} (h : j ≠ k) (d : α) :
    stdBasisMatrix i j c * stdBasisMatrix k l d = 0

Proof state:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
⊢ (∑ x : m, if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0

Tactic:
refine Finset.sum_eq_zero (fun x _ => ?_)

Result:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
x : m
x✝ : x ∈ Finset.univ
⊢ (if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0

Proof state:
case pos.hnc.intro.intro
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h✝ : j ≠ k
d : α
a : l✝
h₁ : i = a
x✝ : k ∈ Finset.univ
h : j = k
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case neg
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : ¬i = a
⊢ (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b

Tactic:
simp only [h₁, false_and, ite_false, mul_ite, zero_mul, mul_zero, ite_self,
  Finset.sum_const_zero, zero_apply]

Result:
no goals

Proof state:
case a
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix k l d) a b = 0 a b

Tactic:
simp only [mul_apply, boole_mul, stdBasisMatrix, of_apply]

Result:
case a
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b

Proof state:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
⊢ (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b

Tactic:
simp only [h₁, true_and, mul_ite, ite_mul, zero_mul, mul_zero, ← ite_and, zero_apply]

Result:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
⊢ (∑ x : m, if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0

Proof state:
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
⊢ stdBasisMatrix i j c * stdBasisMatrix k l d = 0

Tactic:
ext a b

Result:
case a
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix k l d) a b = 0 a b

Proof state:
case pos.hnc
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
x : m
x✝ : x ∈ Finset.univ
⊢ ¬((k = x ∧ l = b) ∧ j = x)

Tactic:
rintro ⟨⟨rfl, rfl⟩, h⟩

Result:
case pos.hnc.intro.intro
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h✝ : j ≠ k
d : α
a : l✝
h₁ : i = a
x✝ : k ∈ Finset.univ
h : j = k
⊢ False

Proof state:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
x : m
x✝ : x ∈ Finset.univ
⊢ (if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0

Tactic:
apply if_neg

Result:
case pos.hnc
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
x : m
x✝ : x ∈ Finset.univ
⊢ ¬((k = x ∧ l = b) ∧ j = x)

Proof state:
case a
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b

Tactic:
by_cases h₁ : i = a

Result:
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
⊢ (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b

case neg
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : ¬i = a
⊢ (∑ x : m, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b