awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
rw :
  Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                (star x) :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Adj i j → x i = x j
rw₁ :
  Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                x :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Adj i j → x i = x j
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
have rw₂ : (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Adj i j → x i = x j
Tactic: rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
⊢ Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                x :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Reachable i j → x i = x j
have rw : (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j
Tactic: rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
⊢ (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j
have refine : (∀ (i j : V), G.Adj i j → x i = x j) → ∀ (i j : V), G.Reachable i j → x i = x j
Tactic: refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
⊢ G.Reachable i j → x i = x j
have this : ∀ (w : G.Walk i j), x i = x j
Tactic: ⟨w⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
w : G.Walk i j
⊢ x i = x j
have nil : ∀ {u : V}, x u = x u
Tactic: induction w with
  | nil => rfl
  | cons hA _ h' => exact (h _ _ hA).trans h'
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
w : G.Walk i j
nil : ∀ {u : V}, x u = x u
⊢ x i = x j
have cons : ∀ {u v w : V} (hA : G.Adj u v) (p : G.Walk v w) (h' : x v = x w), x u = x w
Tactic: induction w with
  | nil => rfl
  | cons hA _ h' => exact (h _ _ hA).trans h'
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
have rw : Eq (α := ℝ)
    (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                      (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                    (lapMatrix ℝ G) :
                  (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
              (star x) :
            (V → ℝ) →ₗ[ℝ] ℝ) :
          (a : V → ℝ) → ℝ)
        x :
      ℝ)
    (0 : ℝ) ↔
  ∀ (i j : V), G.Reachable i j → x i = x j
Tactic: rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
rw :
  Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                (star x) :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Reachable i j → x i = x j
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
have rw₁ : Eq (α := ℝ)
    (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                      (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                    (lapMatrix ℝ G) :
                  (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
              x :
            (V → ℝ) →ₗ[ℝ] ℝ) :
          (a : V → ℝ) → ℝ)
        x :
      ℝ)
    (0 : ℝ) ↔
  ∀ (i j : V), G.Reachable i j → x i = x j
Tactic: rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
rw :
  Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                (star x) :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Reachable i j → x i = x j
rw₁ :
  Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                x :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Reachable i j → x i = x j
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
have rw₂ : (∀ (i j : V), G.Reachable i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j
Tactic: rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ (lapMatrix ℝ G).det = 0
have rw : ∃ (v : V → ℝ), v ≠ 0 ∧ lapMatrix ℝ G *ᵥ v = 0
Tactic: rw [← Matrix.exists_mulVec_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ ∃ (v : V → ℝ), v ≠ 0 ∧ lapMatrix ℝ G *ᵥ v = 0
have h₁ : Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0 ∧ (lapMatrix ℝ G *ᵥ fun (x : V) ↦ 1) = 0
Tactic: use fun _ ↦ 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0 ∧ (lapMatrix ℝ G *ᵥ fun (x : V) ↦ 1) = 0
have h₁ : Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0
Tactic: refine ⟨?_, (lapMatrix_mulVec_eq_zero_iff_forall_adj G).mpr fun _ _ _ ↦ rfl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0
have h₁ : Set.Nonempty.{u_1} (α := V) (Function.support (M := ℝ) fun (x : V) ↦ 1)
Tactic: rw [← Function.support_nonempty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ Set.Nonempty.{u_1} (α := V) (Function.support (M := ℝ) fun (x : V) ↦ 1)
have h₁ : Membership.mem (γ := Set V) (Function.support (M := ℝ) fun (x : V) ↦ 1) (Classical.choice h)
Tactic: use Classical.choice h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
inst_3 : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ Membership.mem (γ := Submodule ℝ (V → ℝ))
    (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
      ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
    fun (i : V) ↦ if G.connectedComponentMk i = c then 1 else 0
have rw : ∀ (i j : V),
  G.Reachable i j →
    Eq (α := ℝ) (if G.connectedComponentMk i = c then 1 else 0) (if G.connectedComponentMk j = c then 1 else 0)
Tactic: rw [LinearMap.mem_ker, toLin'_apply, lapMatrix_mulVec_eq_zero_iff_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
⊢ LinearIndependent ℝ (M :=
    ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
        ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    G.lapMatrix_ker_basis_aux
have rw : ∀ (g : G.ConnectedComponent → ℝ),
  Eq.{u_1 + 1} (α :=
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
      (∑ i : G.ConnectedComponent,
        HSMul.hSMul (β :=
          ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
              ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
          (g i) (G.lapMatrix_ker_basis_aux i))
      0 →
    ∀ (i : G.ConnectedComponent), g i = 0
Tactic: rw [Fintype.linearIndependent_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α :=
    ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
        ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    (∑ i : G.ConnectedComponent,
      HSMul.hSMul (β :=
        ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
            ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
        (g i) (G.lapMatrix_ker_basis_aux i))
    0
⊢ ∀ (i : G.ConnectedComponent), g i = 0
have h0₁ : Eq.{u_1 + 1} (α := V → ℝ)
  (↑(∑ i : G.ConnectedComponent,
        HSMul.hSMul (β :=
          ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
              ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
          (g i) (G.lapMatrix_ker_basis_aux i)) :
    V → ℝ)
  (↑0 : V → ℝ)
Tactic: rw [Subtype.ext_iff] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ i : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g i) (G.lapMatrix_ker_basis_aux i)) :
      V → ℝ)
    (↑0 : V → ℝ)
⊢ Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ c : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g c) (G.lapMatrix_ker_basis_aux c)) :
      V → ℝ)
    fun (i : V) ↦ g (G.connectedComponentMk i)
have simp : Eq.{u_1 + 1} (α := V → ℝ)
  (↑(∑ x : G.ConnectedComponent,
        Subtype.mk (p := fun (x : V → ℝ) ↦
          Membership.mem (γ := Submodule ℝ (V → ℝ))
            (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
              ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
            x)
          (HSMul.hSMul (β := V → ℝ) (g x) fun (i : V) ↦ if G.connectedComponentMk i = x then 1 else 0) sorry) :
    V → ℝ)
  fun (i : V) ↦ g (G.connectedComponentMk i)
Tactic: simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ i : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g i) (G.lapMatrix_ker_basis_aux i)) :
      V → ℝ)
    (↑0 : V → ℝ)
⊢ Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ x : G.ConnectedComponent,
          Subtype.mk (p := fun (x : V → ℝ) ↦
            Membership.mem (γ := Submodule ℝ (V → ℝ))
              (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
              x)
            (HSMul.hSMul (β := V → ℝ) (g x) fun (i : V) ↦ if G.connectedComponentMk i = x then 1 else 0) ⋯) :
      V → ℝ)
    fun (i : V) ↦ g (G.connectedComponentMk i)
have rw : Eq.{u_1 + 1} (α := V → ℝ)
  (∑ i : G.ConnectedComponent,
    (↑(Subtype.mk (p := fun (x : V → ℝ) ↦
          Membership.mem (γ := Submodule ℝ (V → ℝ))
            (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
              ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
            x)
          (HSMul.hSMul (β := V → ℝ) (g i) fun (i_1 : V) ↦ if G.connectedComponentMk i_1 = i then 1 else 0) sorry) :
      V → ℝ))
  fun (i : V) ↦ g (G.connectedComponentMk i)
Tactic: rw [AddSubmonoid.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ i : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g i) (G.lapMatrix_ker_basis_aux i)) :
      V → ℝ)
    (↑0 : V → ℝ)
⊢ Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ x : G.ConnectedComponent,
          Subtype.mk (p := fun (x : V → ℝ) ↦
            Membership.mem (γ := Submodule ℝ (V → ℝ))
              (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
              x)
            (HSMul.hSMul (β := V → ℝ) (g x) fun (i : V) ↦ if G.connectedComponentMk i = x then 1 else 0) ⋯) :
      V → ℝ)
    fun (i : V) ↦ g (G.connectedComponentMk i)
have repeat : Eq.{u_1 + 1} (α := V → ℝ)
  (∑ i : G.ConnectedComponent,
    (↑(Subtype.mk (p := fun (x : V → ℝ) ↦
          Membership.mem (γ := Submodule ℝ (V → ℝ))
            (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
              ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
            x)
          (HSMul.hSMul (β := V → ℝ) (g i) fun (i_1 : V) ↦ if G.connectedComponentMk i_1 = i then 1 else 0) sorry) :
      V → ℝ))
  fun (i : V) ↦ g (G.connectedComponentMk i)
Tactic: repeat rw [AddSubmonoid.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ i : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g i) (G.lapMatrix_ker_basis_aux i)) :
      V → ℝ)
    (↑0 : V → ℝ)
⊢ Eq.{u_1 + 1} (α := V → ℝ)
    (∑ i : G.ConnectedComponent,
      (↑(Subtype.mk (p := fun (x : V → ℝ) ↦
            Membership.mem (γ := Submodule ℝ (V → ℝ))
              (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
              x)
            (HSMul.hSMul (β := V → ℝ) (g i) fun (i_1 : V) ↦ if G.connectedComponentMk i_1 = i then 1 else 0) ⋯) :
        V → ℝ))
    fun (i : V) ↦ g (G.connectedComponentMk i)
have h : ∀ (i : V),
  (∑ i : G.ConnectedComponent,
        (↑(Subtype.mk (p := fun (x : V → ℝ) ↦
              Membership.mem (γ := Submodule ℝ (V → ℝ))
                (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                  ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
                x)
              (HSMul.hSMul (β := V → ℝ) (g i) fun (i_1 : V) ↦ if G.connectedComponentMk i_1 = i then 1 else 0) sorry) :
          V → ℝ))
      i =
    g (G.connectedComponentMk i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ i : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g i) (G.lapMatrix_ker_basis_aux i)) :
      V → ℝ)
    (↑0 : V → ℝ)
⊢ ∀ (i : G.ConnectedComponent), g i = 0
have h : Eq.{u_1 + 1} (α := V → ℝ)
  (↑(∑ c : G.ConnectedComponent,
        HSMul.hSMul (β :=
          ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
              ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
          (g c) (G.lapMatrix_ker_basis_aux c)) :
    V → ℝ)
  fun (i : V) ↦ g (G.connectedComponentMk i)
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]
    repeat rw [AddSubmonoid.coe_finsetSum]
    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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ i : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g i) (G.lapMatrix_ker_basis_aux i)) :
      V → ℝ)
    (↑0 : V → ℝ)
h :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ c : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g c) (G.lapMatrix_ker_basis_aux c)) :
      V → ℝ)
    fun (i : V) ↦ g (G.connectedComponentMk i)
⊢ ∀ (i : G.ConnectedComponent), g i = 0
have h0₁ : Eq.{u_1 + 1} (α := V → ℝ) (fun (i : V) ↦ g (G.connectedComponentMk i)) (↑0 : V → ℝ)
Tactic: rw [h] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : Eq.{u_1 + 1} (α := V → ℝ) (fun (i : V) ↦ g (G.connectedComponentMk i)) (↑0 : V → ℝ)
h :
  Eq.{u_1 + 1} (α := V → ℝ)
    (↑(∑ c : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (g c) (G.lapMatrix_ker_basis_aux c)) :
      V → ℝ)
    fun (i : V) ↦ g (G.connectedComponentMk i)
c : G.ConnectedComponent
⊢ g c = 0
have obtain : ∀ (i : V) (h' : G.connectedComponentMk i = c), g c = 0
Tactic: obtain ⟨i, h'⟩ : ∃ i : V, G.connectedComponentMk i = c := Quot.exists_rep c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
x :
  ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
      ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
h :
  Membership.mem (γ :=
    Submodule ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    ⊤ x
⊢ Membership.mem (γ :=
    Submodule ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    (Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)) x
have rw : ∃ (c : G.ConnectedComponent → ℝ),
  ∑ i : G.ConnectedComponent,
      HSMul.hSMul (β :=
        ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
            ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
        (c i) (G.lapMatrix_ker_basis_aux i) =
    x
Tactic: rw [Submodule.mem_span_range_iff_exists_fun]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : DecidableEq G.ConnectedComponent
x :
  ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
      ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
h :
  Membership.mem (γ :=
    Submodule ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    ⊤ x
⊢ ∀ (a b : V) (a_1 : G.Reachable a b), (↑x : V → ℝ) a = (↑x : V → ℝ) b
have rw : lapMatrix ℝ G *ᵥ (↑x : V → ℝ) = 0
Tactic: rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable,
    ← toLin'_apply, LinearMap.map_coe_ker]