-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
lemma top_le_span_range_lapMatrix_ker_basis_aux :
    ⊤ ≤ Submodule.span ℝ (Set.range (lapMatrix_ker_basis_aux G))

Proof state:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ i : G.ConnectedComponent, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i) j = ↑x j

Tactic:
simp only [lapMatrix_ker_basis_aux]

Result:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ x_1 : G.ConnectedComponent, Quot.lift ↑x ⋯ x_1 • ⟨fun i => if G.connectedComponentMk i = x_1 then 1 else 0, ⋯⟩)
      j =
    ↑x j

Proof state:
case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ ∑ i : G.ConnectedComponent, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i = x

Tactic:
ext j

Result:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ i : G.ConnectedComponent, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i) j = ↑x j

Proof state:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ Quot.lift ↑x ⋯ (G.connectedComponentMk j) = ↑x j

Tactic:
rfl

Result:
no goals

Proof state:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ (∑ i : G.ConnectedComponent, ↑(Quot.lift ↑x ⋯ i • ⟨fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩))
      j =
    ↑x j

Tactic:
simp only [SetLike.mk_smul_mk, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one,
  mul_zero, sum_ite_eq, mem_univ, ↓reduceIte]

Result:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ Quot.lift ↑x ⋯ (G.connectedComponentMk j) = ↑x j

Proof state:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ x_1 : G.ConnectedComponent, Quot.lift ↑x ⋯ x_1 • ⟨fun i => if G.connectedComponentMk i = x_1 then 1 else 0, ⋯⟩)
      j =
    ↑x j

Tactic:
rw [AddSubmonoid.coe_finset_sum]

Result:
case h.a.h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
j : V
⊢ (∑ i : G.ConnectedComponent, ↑(Quot.lift ↑x ⋯ i • ⟨fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩))
      j =
    ↑x j

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

Tactic:
intro x _

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ ∀ (a b : V), G.Reachable a b → ↑x a = ↑x b

Tactic:
rw [← lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable G x,
LinearMap.map_coe_ker]

Result:
no goals

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ ∃ c, ∑ i : G.ConnectedComponent, c i • G.lapMatrix_ker_basis_aux i = x

Tactic:
use Quot.lift x.val (by rw [← lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable G x,
  LinearMap.map_coe_ker])

Result:
case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ ∑ i : G.ConnectedComponent, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i = x

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

Tactic:
rw [mem_span_range_iff_exists_fun]

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
a✝ : x ∈ ⊤
⊢ ∃ c, ∑ i : G.ConnectedComponent, c i • G.lapMatrix_ker_basis_aux i = x