-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes [DecidableEq V] [DecidableEq α]
    [NonAssocSemiring α] : 1 + G.adjMatrix α + (G.adjMatrix α).compl = Matrix.of fun _ _ ↦ 1

Proof state:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
⊢ (1 + adjMatrix α G + fun i j => if i = j then 0 else if adjMatrix α G i j = 0 then 1 else 0) i j =
    of (fun x x => 1) i j

Tactic:
rw [of_apply, add_apply, adjMatrix_apply, add_apply, adjMatrix_apply, one_apply]

Result:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
⊢ (((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) +
      if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) =
    1

Proof state:
case neg
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
h : ¬G.Adj i j
⊢ (((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) +
      if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) =
    1

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
case pos
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
h : G.Adj i j
⊢ (((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) +
      if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) =
    1

Tactic:
aesop

Result:
no goals

Proof state:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
⊢ (1 + adjMatrix α G + (adjMatrix α G).compl) i j = of (fun x x => 1) i j

Tactic:
unfold Matrix.compl

Result:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
⊢ (1 + adjMatrix α G + fun i j => if i = j then 0 else if adjMatrix α G i j = 0 then 1 else 0) i j =
    of (fun x x => 1) i j

Proof state:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
⊢ (((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) +
      if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) =
    1

Tactic:
by_cases h : G.Adj i j

Result:
case pos
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
h : G.Adj i j
⊢ (((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) +
      if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) =
    1

case neg
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
h : ¬G.Adj i j
⊢ (((if i = j then 1 else 0) + if G.Adj i j then 1 else 0) +
      if i = j then 0 else if (if G.Adj i j then 1 else 0) = 0 then 1 else 0) =
    1

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
⊢ 1 + adjMatrix α G + (adjMatrix α G).compl = of fun x x => 1

Tactic:
ext i j

Result:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring α
i j : V
⊢ (1 + adjMatrix α G + (adjMatrix α G).compl) i j = of (fun x x => 1) i j