-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
lemma mem_ker_toLin'_lapMatrix_of_connectedComponent {G : SimpleGraph V} [DecidableRel G.Adj]
    [DecidableEq G.ConnectedComponent] (c : G.ConnectedComponent) :
    (fun i ↦ if connectedComponentMk G i = c then 1 else 0) ∈
      LinearMap.ker (toLin' (lapMatrix ℝ G))

Proof state:
case pos
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : G.connectedComponentMk i = c
h₂ : G.connectedComponentMk j = c
⊢ 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.connectedComponentMk i = G.connectedComponentMk j
h₁ : ¬G.connectedComponentMk i = c
h₃ : G.connectedComponentMk j = c
⊢ 0 = 1

Tactic:
exact (h₁ (h₃ ▸ h)).elim

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : ¬G.connectedComponentMk i = c
h₃ : ¬G.connectedComponentMk j = c
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
⊢ (if G.connectedComponentMk i = c then 1 else 0) = if G.connectedComponentMk j = c then 1 else 0

Tactic:
split_ifs with h₁ h₂ h₃

Result:
case pos
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : G.connectedComponentMk i = c
h₂ : G.connectedComponentMk j = c
⊢ 1 = 1

case neg
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : G.connectedComponentMk i = c
h₂ : ¬G.connectedComponentMk j = c
⊢ 1 = 0

case pos
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : ¬G.connectedComponentMk i = c
h₃ : G.connectedComponentMk j = c
⊢ 0 = 1

case neg
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : ¬G.connectedComponentMk i = c
h₃ : ¬G.connectedComponentMk j = c
⊢ 0 = 0

Proof state:
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ (fun i => if G.connectedComponentMk i = c then 1 else 0) ∈ LinearMap.ker (toLin' (lapMatrix ℝ G))

Tactic:
rw [LinearMap.mem_ker, lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable]

Result:
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ ∀ (i j : V),
    G.Reachable i j → (if G.connectedComponentMk i = c then 1 else 0) = if G.connectedComponentMk j = c then 1 else 0

Proof state:
case neg
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.connectedComponentMk i = G.connectedComponentMk j
h₁ : G.connectedComponentMk i = c
h₂ : ¬G.connectedComponentMk j = c
⊢ 1 = 0

Tactic:
exact (h₂ (h₁ ▸ h.symm)).elim

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : G.connectedComponentMk i = c
h₂ : ¬G.connectedComponentMk j = c
⊢ 1 = 0

Tactic:
rw [← ConnectedComponent.eq] at h

Result:
case neg
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.connectedComponentMk i = G.connectedComponentMk j
h₁ : G.connectedComponentMk i = c
h₂ : ¬G.connectedComponentMk j = c
⊢ 1 = 0

Proof state:
case pos
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
h₁ : ¬G.connectedComponentMk i = c
h₃ : G.connectedComponentMk j = c
⊢ 0 = 1

Tactic:
rw [← ConnectedComponent.eq] at h

Result:
case pos
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.connectedComponentMk i = G.connectedComponentMk j
h₁ : ¬G.connectedComponentMk i = c
h₃ : G.connectedComponentMk j = c
⊢ 0 = 1

Proof state:
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ ∀ (i j : V),
    G.Reachable i j → (if G.connectedComponentMk i = c then 1 else 0) = if G.connectedComponentMk j = c then 1 else 0

Tactic:
intro i j h

Result:
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
i j : V
h : G.Reachable i j
⊢ (if G.connectedComponentMk i = c then 1 else 0) = if G.connectedComponentMk j = c then 1 else 0