-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
lemma linearIndependent_lapMatrix_ker_basis_aux :
    LinearIndependent ℝ (lapMatrix_ker_basis_aux G)

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ x : G.ConnectedComponent, ⟨g x • fun i => if G.connectedComponentMk i = x then 1 else 0, ⋯⟩) = fun i =>
    g (G.connectedComponentMk i)

Tactic:
rw [AddSubmonoid.coe_finset_sum]

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i : G.ConnectedComponent, ↑⟨g i • fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i =>
    g (G.connectedComponentMk i)

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
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
i : V
⊢ (∑ i : G.ConnectedComponent, ↑⟨g i • fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩) i =
    g (G.connectedComponentMk i)

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

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
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
have h : ∑ c, g c • lapMatrix_ker_basis_aux G c = fun i ↦ g (connectedComponentMk G i) := by
  simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk, AddSubmonoid.coe_finset_sum]
  repeat rw [AddSubmonoid.coe_finset_sum]
  ext i
  simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, sum_ite_eq,
    mem_univ, ↓reduceIte]

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ ∀ (g : G.ConnectedComponent → ℝ),
    ∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i = 0 → ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
intro g h0

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i = 0
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i : G.ConnectedComponent, ↑⟨g i • fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i =>
    g (G.connectedComponentMk i)

Tactic:
ext i

Result:
case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
i : V
⊢ (∑ i : G.ConnectedComponent, ↑⟨g i • fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩) i =
    g (G.connectedComponentMk i)

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
rw [h] at h0

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : (fun i => g (G.connectedComponentMk i)) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)

Tactic:
simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk, AddSubmonoid.coe_finset_sum]

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ x : G.ConnectedComponent, ⟨g x • fun i => if G.connectedComponentMk i = x then 1 else 0, ⋯⟩) = fun i =>
    g (G.connectedComponentMk i)

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ x : G.ConnectedComponent, ⟨g x • fun i => if G.connectedComponentMk i = x then 1 else 0, ⋯⟩) = fun i =>
    g (G.connectedComponentMk i)

Tactic:
repeat rw [AddSubmonoid.coe_finset_sum]

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i : G.ConnectedComponent, ↑⟨g i • fun i_1 => if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i =>
    g (G.connectedComponentMk i)

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i = 0
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
rw [Subtype.ext_iff] at h0

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Proof state:
case intro
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : (fun i => g (G.connectedComponentMk i)) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
c : G.ConnectedComponent
i : V
h' : G.connectedComponentMk i = c
⊢ g c = 0

Tactic:
exact h' ▸ congrFun h0 i

Result:
no goals