-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_mul_transpose
    [∀ a, Fintype (neighborSet G a)] [DecidableEq α] [DecidableRel G.Adj] :
    G.incMatrix R * (G.incMatrix R)ᵀ = fun a b =>
      if a = b then (G.degree a : R) else if G.Adj a b then 1 else 0

Proof state:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0

Tactic:
simp only [Matrix.mul_apply, Matrix.transpose_apply,
  G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h', sum_const_zero]

Result:
no goals

Proof state:
case a
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0

Tactic:
split_ifs with h h'

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(G.degree a)

case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ incMatrix R G * (incMatrix R G)ᵀ = fun a b => if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0

Tactic:
ext a b

Result:
case a
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Tactic:
exact incMatrix_mul_transpose_diag (R := R) G

Result:
no goals

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(G.degree a)

Tactic:
subst b

Result:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Proof state:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
inst✝² : (a : α) → Fintype ↑(G.neighborSet a)
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
exact G.incMatrix_mul_transpose_apply_of_adj h'

Result:
no goals