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
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
rw : lapMatrix ℝ G *ᵥ (↑x : V → ℝ) = 0
⊢ ∀ (a b : V) (a_1 : G.Reachable a b), (↑x : V → ℝ) a = (↑x : V → ℝ) b
have rw₁ : Eq (α := V → ℝ)
  ((((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G) : (V → ℝ) →ₗ[ℝ] V → ℝ) : (a : V → ℝ) → V → ℝ)
      (↑x : V → ℝ) :
    V → ℝ)
  (0 : V → ℝ)
Tactic: rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable,
    ← toLin'_apply, LinearMap.map_coe_ker]
-- 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
rw : lapMatrix ℝ G *ᵥ (↑x : V → ℝ) = 0
rw₁ :
  Eq (α := V → ℝ)
    ((((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G) : (V → ℝ) →ₗ[ℝ] V → ℝ) : (a : V → ℝ) → V → ℝ)
        (↑x : V → ℝ) :
      V → ℝ)
    (0 : V → ℝ)
⊢ ∀ (a b : V) (a_1 : G.Reachable a b), (↑x : V → ℝ) a = (↑x : V → ℝ) b
have rw₂ : Eq.{u_1 + 1} (α := V → ℝ) 0 0
Tactic: rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable,
    ← toLin'_apply, LinearMap.map_coe_ker]
-- 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
⊢ ∃ (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
have h : ∑ i : G.ConnectedComponent,
    HSMul.hSMul (β :=
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
      (Quot.lift (r := G.Reachable) (↑x : V → ℝ) sorry i) (G.lapMatrix_ker_basis_aux i) =
  x
Tactic: use Quot.lift x.val (by rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable,
    ← toLin'_apply, LinearMap.map_coe_ker])
-- 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
⊢ ∑ i : G.ConnectedComponent,
      HSMul.hSMul (β :=
        ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
            ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
        (Quot.lift (r := G.Reachable) (↑x : V → ℝ) ⋯ i) (G.lapMatrix_ker_basis_aux i) =
    x
have h : ∀ (j : V),
  (↑(∑ i : G.ConnectedComponent,
            HSMul.hSMul (β :=
              ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                  ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
              (Quot.lift (r := G.Reachable) (↑x : V → ℝ) sorry i) (G.lapMatrix_ker_basis_aux i)) :
        V → ℝ)
      j =
    (↑x : V → ℝ) j
Tactic: ext j
-- 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
j : V
⊢ (↑(∑ i : G.ConnectedComponent,
            HSMul.hSMul (β :=
              ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                  ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
              (Quot.lift (r := G.Reachable) (↑x : V → ℝ) ⋯ i) (G.lapMatrix_ker_basis_aux i)) :
        V → ℝ)
      j =
    (↑x : V → ℝ) j
have h : (↑(∑ x_1 : G.ConnectedComponent,
          HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (Quot.lift (r := G.Reachable) (↑x : V → ℝ) sorry x_1)
            (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)
              (fun (i : V) ↦ if G.connectedComponentMk i = x_1 then 1 else 0) sorry)) :
      V → ℝ)
    j =
  (↑x : V → ℝ) j
Tactic: simp only [lapMatrix_ker_basis_aux]
-- 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
j : V
⊢ (↑(∑ x_1 : G.ConnectedComponent,
            HSMul.hSMul (β :=
              ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                  ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
              (Quot.lift (r := G.Reachable) (↑x : V → ℝ) ⋯ x_1)
              (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)
                (fun (i : V) ↦ if G.connectedComponentMk i = x_1 then 1 else 0) ⋯)) :
        V → ℝ)
      j =
    (↑x : V → ℝ) j
have h : (∑ i : G.ConnectedComponent,
      (↑(HSMul.hSMul (β :=
            ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
            (Quot.lift (r := G.Reachable) (↑x : V → ℝ) sorry i)
            (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)
              (fun (i_1 : V) ↦ if G.connectedComponentMk i_1 = i then 1 else 0) sorry)) :
        V → ℝ))
    j =
  (↑x : V → ℝ) j
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
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
j : V
⊢ (∑ i : G.ConnectedComponent,
        (↑(HSMul.hSMul (β :=
              ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
                  ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
              (Quot.lift (r := G.Reachable) (↑x : V → ℝ) ⋯ i)
              (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)
                (fun (i_1 : V) ↦ if G.connectedComponentMk i_1 = i then 1 else 0) ⋯)) :
          V → ℝ))
      j =
    (↑x : V → ℝ) j
have h : Quot.lift (r := G.Reachable) (↑x : V → ℝ) sorry (G.connectedComponentMk j) = (↑x : V → ℝ) 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]
-- 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
⊢ Fintype.card.{u_1} G.ConnectedComponent =
    finrank.{0, u_1} ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
have rw : Fintype.card.{u_1} G.ConnectedComponent = Fintype.card.{u_1} G.ConnectedComponent
Tactic: rw [Module.finrank_eq_card_basis G.lapMatrix_ker_basis]
-- 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
⊢ Fintype.card.{u_1} G.ConnectedComponent =
    finrank.{0, u_1} ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
have rw : Fintype.card.{u_1} G.ConnectedComponent = Fintype.card.{u_1} G.ConnectedComponent
Tactic: classical
  rw [Module.finrank_eq_card_basis G.lapMatrix_ker_basis]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LineGraph (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
e₁ e₂ : (↑G.edgeSet : Type u_1)
h : e₁ ≠ e₂ ∧ ((↑(↑e₁ : Sym2 V) : Set V) ∩ (↑(↑e₂ : Sym2 V) : Set V)).Nonempty
⊢ e₂ ≠ e₁ ∧ ((↑(↑e₂ : Sym2 V) : Set V) ∩ (↑(↑e₁ : Sym2 V) : Set V)).Nonempty
have rwa : e₁ ≠ e₂ ∧ ((↑(↑e₂ : Sym2 V) : Set V) ∩ (↑(↑e₁ : Sym2 V) : Set V)).Nonempty
Tactic: rwa [ne_comm, Set.inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LineGraph (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
e : (↑G.edgeSet : Type u_1)
⊢ Sym2.map (⇑f : (a : V) → V') (↑e : Sym2 V) ∈ G'.edgeSet
have mk : ∀ (val : Sym2 V) (a : V × V) (h : Quot.mk (Sym2.Rel V) a ∈ G.edgeSet),
  Sym2.map (⇑f : (a : V) → V')
      (↑(Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h) : Sym2 V) ∈
    G'.edgeSet
Tactic: rcases e with ⟨⟨⟩, h⟩
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LineGraph (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
⊢ ∀ {a b : (↑G.edgeSet : Type u_1)},
    G'.lineGraph.Adj
        (({
              toFun := fun (e : (↑G.edgeSet : Type u_1)) ↦
                Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑e : Sym2 V)) ⋯,
              inj' := ⋯ } :
            (a : (↑G.edgeSet : Type u_1)) → (↑G'.edgeSet : Type u_2))
          a)
        (({
              toFun := fun (e : (↑G.edgeSet : Type u_1)) ↦
                Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑e : Sym2 V)) ⋯,
              inj' := ⋯ } :
            (a : (↑G.edgeSet : Type u_1)) → (↑G'.edgeSet : Type u_2))
          b) ↔
      G.lineGraph.Adj a b
have simp : ∀ {a b : (↑G.edgeSet : Type u_1)},
  ¬Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑a : Sym2 V)) sorry =
          Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑b : Sym2 V)) sorry ∧
      Set.Nonempty.{u_2} (α := V')
        ((⇑f : (a : V) → V') '' (↑(↑a : Sym2 V) : Set V) ∩ (⇑f : (a : V) → V') '' (↑(↑b : Sym2 V) : Set V)) ↔
    ¬a = b ∧ ((↑(↑a : Sym2 V) : Set V) ∩ (↑(↑b : Sym2 V) : Set V)).Nonempty
Tactic: simp only [lineGraph, Function.Embedding.coeFn_mk, Sym2.coe_map, ne_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LineGraph (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
⊢ ∀ {a b : (↑G.edgeSet : Type u_1)},
    ¬Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑a : Sym2 V)) ⋯ =
            Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑b : Sym2 V)) ⋯ ∧
        Set.Nonempty.{u_2} (α := V')
          ((⇑f : (a : V) → V') '' (↑(↑a : Sym2 V) : Set V) ∩ (⇑f : (a : V) → V') '' (↑(↑b : Sym2 V) : Set V)) ↔
      ¬a = b ∧ ((↑(↑a : Sym2 V) : Set V) ∩ (↑(↑b : Sym2 V) : Set V)).Nonempty
have refine : ∀ {a b : (↑G.edgeSet : Type u_1)},
  ¬Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑a : Sym2 V)) sorry =
        Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑b : Sym2 V)) sorry ↔
    ¬a = b
Tactic: refine .and ?_ <| Set.image_inter f.injective ▸ Set.image_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LineGraph (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
a b : (↑G.edgeSet : Type u_1)
⊢ ¬Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑a : Sym2 V)) ⋯ =
        Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑b : Sym2 V)) ⋯ ↔
    ¬a = b
have rw : ¬Eq.{u_2 + 1} (α := Sym2 V') (Sym2.map (⇑f : (a : V) → V') (↑a : Sym2 V)) (Sym2.map (⇑f : (a : V) → V') (↑b : Sym2 V)) ↔
  ¬(↑a : Sym2 V) = (↑b : Sym2 V)
Tactic: rw [Subtype.mk.injEq, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ Eq.{u_2 + 1} (α := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G))
    ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet)
have h : ∀ (v : Sym2 W),
  Membership.mem (γ := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G)) v ↔
    Membership.mem (γ := Set (Sym2 W)) ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
v : Sym2 W
⊢ Membership.mem (γ := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G)) v ↔
    Membership.mem (γ := Set (Sym2 W)) ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet) v
have h : ∀ (x y : W),
  Membership.mem (γ := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G)) s(x, y) ↔
    Membership.mem (γ := Set (Sym2 W)) ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet) s(x, y)
Tactic: induction v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
⊢ Membership.mem (γ := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G)) s(x, y) ↔
    Membership.mem (γ := Set (Sym2 W)) ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet) s(x, y)
have h : (∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y) ↔
  ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)
Tactic: rw [mem_edgeSet, map_adj, Set.mem_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
⊢ (∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y) ↔
    ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)
have h : (∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y) →
  ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
h :
  (∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y) →
    ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)
⊢ (∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y) ↔
    ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)
have h₁ : (∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)) →
  ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
a b : V
hadj : G.Adj a b
ha : (f : (a : V) → W) a = x
hb : (f : (a : V) → W) b = y
⊢ ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)
have right : (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)
Tactic: use s(a, b), hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
a b : V
hadj : G.Adj a b
ha : (f : (a : V) → W) a = x
hb : (f : (a : V) → W) b = y
⊢ (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)
have right : Sym2.map (⇑f : (a : V) → W) s(a, b) = s(x, y)
Tactic: rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
a b : V
hadj : G.Adj a b
ha : (f : (a : V) → W) a = x
hb : (f : (a : V) → W) b = y
right : Sym2.map (⇑f : (a : V) → W) s(a, b) = s(x, y)
⊢ (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)
have right₁ : s((f : (a : V) → W) a, (f : (a : V) → W) b) = s(x, y)
Tactic: rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
a b : V
hadj : G.Adj a b
ha : (f : (a : V) → W) a = x
hb : (f : (a : V) → W) b = y
right : Sym2.map (⇑f : (a : V) → W) s(a, b) = s(x, y)
right₁ : s((f : (a : V) → W) a, (f : (a : V) → W) b) = s(x, y)
⊢ (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)
have right₂ : s(x, (f : (a : V) → W) b) = s(x, y)
Tactic: rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
a b : V
hadj : G.Adj a b
ha : (f : (a : V) → W) a = x
hb : (f : (a : V) → W) b = y
right : Sym2.map (⇑f : (a : V) → W) s(a, b) = s(x, y)
right₁ : s((f : (a : V) → W) a, (f : (a : V) → W) b) = s(x, y)
right₂ : s(x, (f : (a : V) → W) b) = s(x, y)
⊢ (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)
have right₃ : s(x, y) = s(x, y)
Tactic: rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
e : Sym2 V
hadj : e ∈ G.edgeSet
he : (f.sym2Map : (a : Sym2 V) → Sym2 W) e = s(x, y)
⊢ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y
have h : ∀ (x_1 y_1 : V) (hadj : s(x_1, y_1) ∈ G.edgeSet) (he : (f.sym2Map : (a : Sym2 V) → Sym2 W) s(x_1, y_1) = s(x, y)),
  ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y
Tactic: induction e
Cleared hypotheses: e, hadj, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (hypothesis)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
x_1 y_1 : V
hadj : s(x_1, y_1) ∈ G.edgeSet
he : (f.sym2Map : (a : Sym2 V) → Sym2 W) s(x_1, y_1) = s(x, y)
⊢ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y
have he₁ : (f : (a : V) → W) x_1 = x ∧ (f : (a : V) → W) y_1 = y ∨ (f : (a : V) → W) x_1 = y ∧ (f : (a : V) → W) y_1 = x
Tactic: rw [Embedding.sym2Map_apply, Sym2.map_mk, Sym2.eq_iff] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
⊢ Eq.{u_2 + 1} (α := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W)
    ((⇑f : (a : V) → W) '' G.neighborSet v : Set W)
have refine_1 : ∀ (u : W),
  Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u →
    Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u
Tactic: refine Set.ext fun u ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
refine_1 :
  ∀ (u : W),
    Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u →
      Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u
⊢ Eq.{u_2 + 1} (α := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W)
    ((⇑f : (a : V) → W) '' G.neighborSet v : Set W)
have refine_2 : ∀ (u : W),
  Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u →
    Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u
Tactic: refine Set.ext fun u ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ SimpleGraph.map id G = G
have Adj : ∀ (x x_1 : V), (SimpleGraph.map id G).Adj x x_1 ↔ G.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
⊢ (SimpleGraph.map id G).Adj x x_1 ↔ G.Adj x x_1
have Adj : (¬x = x_1 ∧ ∃ (a : V) (b : V), G.Adj a b ∧ a = x ∧ b = x_1) ↔ G.Adj x x_1
Tactic: dsimp [SimpleGraph.map, Relation.Map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
⊢ SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (g ∘ f) G
have Adj : ∀ (x x_1 : X), (SimpleGraph.map g (SimpleGraph.map f G)).Adj x x_1 ↔ (SimpleGraph.map (g ∘ f) G).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
x x_1 : X
⊢ (SimpleGraph.map g (SimpleGraph.map f G)).Adj x x_1 ↔ (SimpleGraph.map (g ∘ f) G).Adj x x_1
have Adj : (¬x = x_1 ∧
    ∃ (a : W) (b : W), (¬a = b ∧ ∃ (a_1 : V) (b_1 : V), G.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∧ g a = x ∧ g b = x_1) ↔
  ¬x = x_1 ∧ ∃ (a : V) (b : V), G.Adj a b ∧ g (f a) = x ∧ g (f b) = x_1
Tactic: dsimp [SimpleGraph.map, Relation.Map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Maps (goal)
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ Eq.{u_2 + 1} (α := Set W) (support (SimpleGraph.map (⇑f : (a : V) → W) G)) ((⇑f : (a : V) → W) '' G.support)
have h : ∀ (x : W),
  Membership.mem (γ := Set W) (support (SimpleGraph.map (⇑f : (a : V) → W) G)) x ↔
    Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.support) x
Tactic: ext