awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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_1 :
  Membership.mem (γ :=
    Submodule ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    ⊤ x
j : V
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 → ℝ) ⋯ 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
⊢ (↑(∑ 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

Tactic:
simp only [lapMatrix_ker_basis_aux]

Premises used: SimpleGraph.lapMatrix_ker_basis_aux
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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_1 :
  Membership.mem (γ :=
    Submodule ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    ⊤ x
j : V
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 → ℝ) ⋯ 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
⊢ (↑(∑ 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

Tactic:
rw [AddSubmonoid.coe_finsetSum]

Premises used: AddSubmonoid.coe_finsetSum
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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_1 :
  Membership.mem (γ :=
    Submodule ℝ
      ↥(LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
          ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G))))
    ⊤ x
j : V
h : Quot.lift (r := G.Reachable) (↑x : V → ℝ) ⋯ (G.connectedComponentMk j) = (↑x : V → ℝ) j
⊢ (∑ 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

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]

Premises used: Finset.mem_univ, Finset.sum_apply, mul_ite, MulZeroClass.mul_zero, reduceIte, smul_eq_mul, mul_one, Finset.sum_ite_eq, SetLike.mk_smul_mk, Pi.smul_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
⊢ Quot.lift (r := G.Reachable) (↑x : V → ℝ) ⋯ (G.connectedComponentMk j) = (↑x : V → ℝ) j

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
rw rw₁ : Fintype.card.{u_1} G.ConnectedComponent = Fintype.card.{u_1} G.ConnectedComponent
⊢ 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)))

Tactic:
rw [Module.finrank_eq_card_basis G.lapMatrix_ker_basis]

Premises used: Module.finrank_eq_card_basis, SimpleGraph.lapMatrix_ker_basis
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
rw rw₁ : Fintype.card.{u_1} G.ConnectedComponent = Fintype.card.{u_1} G.ConnectedComponent
⊢ 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)))

Tactic:
classical
  rw [Module.finrank_eq_card_basis G.lapMatrix_ker_basis]
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
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
rwa : e₁ ≠ e₂ ∧ ((↑(↑e₂ : Sym2 V) : Set V) ∩ (↑(↑e₁ : Sym2 V) : Set V)).Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : 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

Tactic:
rwa [ne_comm, Set.inter_comm]

Premises used: Set.inter_comm, ne_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
G : SimpleGraph V
e₁ e₂ : (↑G.edgeSet : Type u_1)
⊢ G.lineGraph.Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v ∈ (↑e₁ : Sym2 V), v ∈ (↑e₂ : Sym2 V)

Tactic:
simp [Set.Nonempty, lineGraph]

Premises used: Set.Nonempty, SimpleGraph.lineGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph (↑(edgeSet ⊥) : Type u_1)) (lineGraph ⊥) ⊥

Tactic:
aesop (add simp lineGraph)

Premises used: SimpleGraph.lineGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
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)
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
⊢ Sym2.map (⇑f : (a : V) → V') (↑e : Sym2 V) ∈ G'.edgeSet

Tactic:
rcases e with ⟨⟨⟩, h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
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:
f.toHom.map_adj h

Premises used: Set.Mem, setOf, SimpleGraph.Hom.map_adj, SimpleGraph.Copy.toHom, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
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:
exact f.toHom.map_adj h

Premises used: SimpleGraph.Hom.map_adj, SimpleGraph.Copy.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
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)) ⋯ =
            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
⊢ ∀ {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

Tactic:
simp only [lineGraph, Function.Embedding.coeFn_mk, Sym2.coe_map, ne_eq]

Premises used: ne_eq, Function.Embedding.coeFn_mk, SimpleGraph.lineGraph, Sym2.coe_map
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
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

Tactic:
.and ?_ <| Set.image_inter f.injective ▸ Set.image_nonempty

Premises used: Set.image_nonempty, SimpleGraph.Copy.injective, Eq.rec, Set.image_inter, Iff.and
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
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)) ⋯ =
          Subtype.mk (p := fun (x : Sym2 V') ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → V') (↑b : Sym2 V)) ⋯ ↔
      ¬a = b
⊢ ∀ {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

Tactic:
refine .and ?_ <| Set.image_inter f.injective ▸ Set.image_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
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)
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)
⊢ ¬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

Tactic:
rw [Subtype.mk.injEq, Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
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)
⊢ ¬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:
Sym2.map.injective f.injective |>.eq_iff.not

Premises used: Sym2.map.injective, Function.Injective.eq_iff, SimpleGraph.Copy.injective, Iff.not
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
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)
⊢ ¬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:
exact Sym2.map.injective f.injective |>.eq_iff.not

Premises used: Sym2.map.injective, Function.Injective.eq_iff, SimpleGraph.Copy.injective, Iff.not
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
h : G ⊴ G'
⊢ G.lineGraph ⊴ G'.lineGraph

Tactic:
⟨h.some.toCopy.toLineGraphEmbedding⟩

Premises used: SimpleGraph.Copy.toLineGraphEmbedding, Nonempty.some, SimpleGraph.IsIndContained, Nonempty.intro, SimpleGraph.Embedding.toCopy
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
h : G ⊑ G'
⊢ G.lineGraph ⊴ G'.lineGraph

Tactic:
⟨h.some.toLineGraphEmbedding⟩

Premises used: SimpleGraph.Copy.toLineGraphEmbedding, Nonempty.some, SimpleGraph.IsIndContained, Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
h : G ⊑ G'
⊢ G.lineGraph ⊑ G'.lineGraph

Tactic:
⟨h.some.lineGraph⟩

Premises used: Nonempty.some, Nonempty.intro, SimpleGraph.Copy.lineGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
x : (↑G.edgeSet : Type u_1)
⊢ (f.symm.toCopy.lineGraph : (a : (↑G'.edgeSet : Type u_2)) → (↑G.edgeSet : Type u_1))
      ((f.toCopy.lineGraph : (a : (↑G.edgeSet : Type u_1)) → (↑G'.edgeSet : Type u_2)) x) =
    x

Tactic:
simp [Copy.lineGraph, Copy.toLineGraphEmbedding, Sym2.map_map]

Premises used: SimpleGraph.Copy.toLineGraphEmbedding, Sym2.map_map, SimpleGraph.Copy.lineGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
x : (↑G'.edgeSet : Type u_2)
⊢ (f.toCopy.lineGraph : (a : (↑G.edgeSet : Type u_1)) → (↑G'.edgeSet : Type u_2))
      ((f.symm.toCopy.lineGraph : (a : (↑G'.edgeSet : Type u_2)) → (↑G.edgeSet : Type u_1)) x) =
    x

Tactic:
simp [Copy.lineGraph, Copy.toLineGraphEmbedding, Sym2.map_map]

Premises used: SimpleGraph.Copy.toLineGraphEmbedding, Sym2.map_map, SimpleGraph.Copy.lineGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
val : Sym2 V
a : V × V
h₁ : Quot.mk (Sym2.Rel V) a ∈ G.edgeSet
val_1 : Sym2 V
a_1 : V × V
h₂ : Quot.mk (Sym2.Rel V) a_1 ∈ G.edgeSet
hne :
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁ ≠
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂
hinter :
  ((↑(↑(Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁) : Sym2 V) : Set V) ∩
      (↑(↑(Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂) : Sym2 V) :
        Set V)).Nonempty
hne' :
  Ne (α := Sym2 V)
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁) :
      Sym2 V)
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂) :
      Sym2 V)
⊢ Adj (V := Sym2 V)
    (SimpleGraph.map (⇑(subtype fun (x : Sym2 V) ↦ x ∈ G'.edgeSet) : (a : { x : Sym2 V // x ∈ G'.edgeSet }) → Sym2 V)
        G'.lineGraph :
      SimpleGraph (Sym2 V))
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁) :
      Sym2 V)
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂) :
      Sym2 V)

Tactic:
⟨hne', ⟨⟨_, h h₁⟩, ⟨_, h h₂⟩, ⟨(hne <| Subtype.ext <| Subtype.mk.inj ·), hinter⟩, rfl, rfl⟩⟩

Premises used: Subtype.mk.inj, Subtype.mk, And.intro, Exists.intro, rfl, Subtype.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.LineGraph
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
val : Sym2 V
a : V × V
h₁ : Quot.mk (Sym2.Rel V) a ∈ G.edgeSet
val_1 : Sym2 V
a_1 : V × V
h₂ : Quot.mk (Sym2.Rel V) a_1 ∈ G.edgeSet
hne :
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁ ≠
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂
hinter :
  ((↑(↑(Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁) : Sym2 V) : Set V) ∩
      (↑(↑(Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂) : Sym2 V) :
        Set V)).Nonempty
hne' :
  Ne (α := Sym2 V)
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁) :
      Sym2 V)
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂) :
      Sym2 V)
⊢ Adj (V := Sym2 V)
    (SimpleGraph.map (⇑(subtype fun (x : Sym2 V) ↦ x ∈ G'.edgeSet) : (a : { x : Sym2 V // x ∈ G'.edgeSet }) → Sym2 V)
        G'.lineGraph :
      SimpleGraph (Sym2 V))
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) h₁) :
      Sym2 V)
    ((subtype fun (x : Sym2 V) ↦ x ∈ G.edgeSet : (a : { x : Sym2 V // x ∈ G.edgeSet }) → Sym2 V)
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) h₂) :
      Sym2 V)

Tactic:
exact ⟨hne', ⟨⟨_, h h₁⟩, ⟨_, h h₂⟩, ⟨(hne <| Subtype.ext <| Subtype.mk.inj ·), hinter⟩, rfl, rfl⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G_1 : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
f : V → W
G : SimpleGraph V
a b : W
v : a ≠ b
w h : V
h_1 : G.Adj w h ∧ f w = a ∧ f h = b
⊢ (Ne ⊓ Relation.Map G.Adj f f) b a

Tactic:
aesop (add norm unfold Relation.Map) (add forward safe Adj.symm)

Premises used: SimpleGraph.Adj.symm, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
u v : W
⊢ (¬u = v ∧ ∃ (a : V) (b : V), G.Adj a b ∧ (f : (a : V) → W) a = u ∧ (f : (a : V) → W) b = v) ↔
    ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = u ∧ (f : (a : V) → W) v' = v

Tactic:
grind [SimpleGraph.Adj.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
G : SimpleGraph V
u v : W
⊢ (SimpleGraph.map f G).Adj u v ↔ u ≠ v ∧ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ f u' = u ∧ f v' = v

Tactic:
Iff.rfl

Premises used: Iff.rfl, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
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
⊢ Eq.{u_2 + 1} (α := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G))
    ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet)

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
v : Sym2 W
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)
⊢ 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:
induction v
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
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)
⊢ 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:
rw [mem_edgeSet, map_adj, Set.mem_image]

Premises used: Set.mem_image, SimpleGraph.map_adj, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
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)
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
⊢ (∃ (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
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
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 : (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)
⊢ ∃ x_1 ∈ G.edgeSet, (f.sym2Map : (a : Sym2 V) → Sym2 W) x_1 = s(x, y)

Tactic:
use s(a, b), hadj