[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : Adj G v w
v✝ w✝ : V
h : (fun a b => Quotient.mk (?m.1383 G hvw a b) (v, w) = Quotient.mk (?m.1383 G hvw a b) (a, b)) v✝ w✝
⊢ Adj G v✝ w✝
[PROOFSTEP]
rw [← G.mem_edgeSet, ← h]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : Adj G v w
v✝ w✝ : V
h : (fun a b => Quotient.mk (Sym2.Rel.setoid V) (v, w) = Quotient.mk (Sym2.Rel.setoid V) (a, b)) v✝ w✝
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
[PROOFSTEP]
exact hvw
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : Adj G v w
a b : V
h : (fun a b => Quotient.mk (Sym2.Rel.setoid V) (v, w) = Quotient.mk (Sym2.Rel.setoid V) (a, b)) a b
⊢ a ∈ {v, w}
[PROOFSTEP]
apply_fun fun e ↦ a ∈ e at h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : Adj G v w
a b : V
h : (a ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)) = (a ∈ Quotient.mk (Sym2.Rel.setoid V) (a, b))
⊢ a ∈ {v, w}
[PROOFSTEP]
simp only [Sym2.mem_iff, true_or, eq_iff_iff, iff_true] at h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : Adj G v w
a b : V
h : a = v ∨ a = w
⊢ a ∈ {v, w}
[PROOFSTEP]
exact h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
⊢ Subgraph.spanningCoe G₁ = Subgraph.spanningCoe G₂ ↔ G₁.Adj = G₂.Adj
[PROOFSTEP]
simp [Subgraph.spanningCoe]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he : e ∈ edgeSet G'
hv : v ∈ e
⊢ v ∈ G'.verts
[PROOFSTEP]
revert hv
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he : e ∈ edgeSet G'
⊢ v ∈ e → v ∈ G'.verts
[PROOFSTEP]
refine' Sym2.ind (fun v w he ↦ _) e he
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
⊢ v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w) → v✝ ∈ G'.verts
[PROOFSTEP]
intro hv
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
hv : v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ v✝ ∈ G'.verts
[PROOFSTEP]
rcases Sym2.mem_iff.mp hv with (rfl | rfl)
[GOAL]
case inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he✝ : e ∈ edgeSet G'
w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
hv : v ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ v ∈ G'.verts
[PROOFSTEP]
exact G'.edge_vert he
[GOAL]
case inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edgeSet G'
hv : v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝)
⊢ v✝ ∈ G'.verts
[PROOFSTEP]
exact G'.edge_vert (G'.symm he)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
⊢ ∀ {v w : V}, (fun a b => ∃ G', G' ∈ s ∧ Adj G' a b) v w → SimpleGraph.Adj G v w
[PROOFSTEP]
rintro a b ⟨G', -, hab⟩
[GOAL]
case intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a✝ b✝ : V
s : Set (Subgraph G)
a b : V
G' : Subgraph G
hab : Adj G' a b
⊢ SimpleGraph.Adj G a b
[PROOFSTEP]
exact G'.adj_sub hab
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
⊢ ∀ {v w : V}, (fun a b => ∃ G', G' ∈ s ∧ Adj G' a b) v w → v ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), G'.verts
[PROOFSTEP]
rintro a b ⟨G', hG', hab⟩
[GOAL]
case intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a✝ b✝ : V
s : Set (Subgraph G)
a b : V
G' : Subgraph G
hG' : G' ∈ s
hab : Adj G' a b
⊢ a ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), G'.verts
[PROOFSTEP]
exact Set.mem_iUnion₂_of_mem hG' (G'.edge_vert hab)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a✝ b✝ : V
s : Set (Subgraph G)
a b : V
h : (fun a b => ∃ G', G' ∈ s ∧ Adj G' a b) a b
⊢ (fun a b => ∃ G', G' ∈ s ∧ Adj G' a b) b a
[PROOFSTEP]
simpa [adj_comm] using h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
⊢ Adj (⨆ (i : ι), f i) a b ↔ ∃ i, Adj (f i) a b
[PROOFSTEP]
simp [iSup]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
⊢ Adj (⨅ (i : ι), f i) a b ↔ (∀ (i : ι), Adj (f i) a b) ∧ SimpleGraph.Adj G a b
[PROOFSTEP]
simp [iInf]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
hs : Set.Nonempty s
⊢ (∀ (G' : Subgraph G), G' ∈ s → Adj G' a b) → SimpleGraph.Adj G a b
[PROOFSTEP]
obtain ⟨G', hG'⟩ := hs
[GOAL]
case intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
G' : Subgraph G
hG' : G' ∈ s
⊢ (∀ (G' : Subgraph G), G' ∈ s → Adj G' a b) → SimpleGraph.Adj G a b
[PROOFSTEP]
exact fun h => G'.adj_sub (h _ hG')
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝ : Nonempty ι
f : ι → Subgraph G
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), Adj (f i) a b
[PROOFSTEP]
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝ : Nonempty ι
f : ι → Subgraph G
⊢ (∀ (G' : Subgraph G), (G' ∈ Set.range fun i => f i) → Adj G' a b) ↔ ∀ (i : ι), Adj (f i) a b
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
⊢ (⨆ (i : ι), f i).verts = ⋃ (i : ι), (f i).verts
[PROOFSTEP]
simp [iSup]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
⊢ (⨅ (i : ι), f i).verts = ⋂ (i : ι), (f i).verts
[PROOFSTEP]
simp [iInf]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
⊢ Function.Injective fun G' => (G'.verts, Subgraph.spanningCoe G')
[PROOFSTEP]
intro G₁ G₂ h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁✝ G₂✝ : Subgraph G
a b : V
G₁ G₂ : Subgraph G
h : (fun G' => (G'.verts, Subgraph.spanningCoe G')) G₁ = (fun G' => (G'.verts, Subgraph.spanningCoe G')) G₂
⊢ G₁ = G₂
[PROOFSTEP]
rw [Prod.ext_iff] at h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁✝ G₂✝ : Subgraph G
a b : V
G₁ G₂ : Subgraph G
h :
  ((fun G' => (G'.verts, Subgraph.spanningCoe G')) G₁).fst = ((fun G' => (G'.verts, Subgraph.spanningCoe G')) G₂).fst ∧
    ((fun G' => (G'.verts, Subgraph.spanningCoe G')) G₁).snd = ((fun G' => (G'.verts, Subgraph.spanningCoe G')) G₂).snd
⊢ G₁ = G₂
[PROOFSTEP]
exact Subgraph.ext _ _ h.1 (spanningCoe_inj.1 h.2)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
src✝ : DistribLattice (Subgraph G) := distribLattice
s : Set (Subgraph G)
G' : Subgraph G
hG' : G' ∈ s
⊢ G'.verts ⊆ (sSup s).verts
[PROOFSTEP]
apply Set.subset_iUnion₂ G' hG'
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
src✝ : DistribLattice (Subgraph G) := distribLattice
s : Set (Subgraph G)
G' : Subgraph G
hG' : ∀ (b : Subgraph G), b ∈ s → b ≤ G'
⊢ ∀ ⦃v w : V⦄, Adj (sSup s) v w → Adj G' v w
[PROOFSTEP]
rintro a b ⟨H, hH, hab⟩
[GOAL]
case intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a✝ b✝ : V
src✝ : DistribLattice (Subgraph G) := distribLattice
s : Set (Subgraph G)
G' : Subgraph G
hG' : ∀ (b : Subgraph G), b ∈ s → b ≤ G'
a b : V
H : Subgraph G
hH : H ∈ s
hab : Adj H a b
⊢ Adj G' a b
[PROOFSTEP]
exact (hG' _ hH).2 hab
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
src✝ : DistribLattice (Subgraph G) := distribLattice
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → Subgraph G
⊢ (⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b).verts = (⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)).verts
[PROOFSTEP]
simpa using iInf_iSup_eq
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
src✝ : DistribLattice (Subgraph G) := distribLattice
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → Subgraph G
⊢ (⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b).Adj = (⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)).Adj
[PROOFSTEP]
ext
[GOAL]
case h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
src✝ : DistribLattice (Subgraph G) := distribLattice
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → Subgraph G
x✝¹ x✝ : V
⊢ Adj (⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b) x✝¹ x✝ ↔ Adj (⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)) x✝¹ x✝
[PROOFSTEP]
simp [Classical.skolem]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v : V
⊢ neighborSet (sSup s) v = ⋃ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v
[PROOFSTEP]
ext
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v x✝ : V
⊢ x✝ ∈ neighborSet (sSup s) v ↔ x✝ ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v : V
⊢ neighborSet (sInf s) v = (⋂ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v) ∩ SimpleGraph.neighborSet G v
[PROOFSTEP]
ext
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v x✝ : V
⊢ x✝ ∈ neighborSet (sInf s) v ↔ x✝ ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v) ∩ SimpleGraph.neighborSet G v
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
v : V
⊢ neighborSet (⨆ (i : ι), f i) v = ⋃ (i : ι), neighborSet (f i) v
[PROOFSTEP]
simp [iSup]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
v : V
⊢ neighborSet (⨅ (i : ι), f i) v = (⋂ (i : ι), neighborSet (f i) v) ∩ SimpleGraph.neighborSet G v
[PROOFSTEP]
simp [iInf]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
⊢ ∀ (x y : V), Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet ⊥ ↔ Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ ∅
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
H₁ H₂ : Subgraph G
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet (H₁ ⊓ H₂) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet H₁ ∩ edgeSet H₂
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
H₁ H₂ : Subgraph G
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet (H₁ ⊔ H₂) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet H₁ ∪ edgeSet H₂
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
⊢ edgeSet (sSup s) = ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
[PROOFSTEP]
ext e
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
e : Sym2 V
⊢ e ∈ edgeSet (sSup s) ↔ e ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
[PROOFSTEP]
induction e using Sym2.ind
[GOAL]
case h.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
x✝ y✝ : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ edgeSet (sSup s) ↔
    Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
⊢ edgeSet (sInf s) = (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
[PROOFSTEP]
ext e
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
e : Sym2 V
⊢ e ∈ edgeSet (sInf s) ↔ e ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
[PROOFSTEP]
induction e using Sym2.ind
[GOAL]
case h.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
x✝ y✝ : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ edgeSet (sInf s) ↔
    Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
⊢ edgeSet (⨆ (i : ι), f i) = ⋃ (i : ι), edgeSet (f i)
[PROOFSTEP]
simp [iSup]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
⊢ edgeSet (⨅ (i : ι), f i) = (⋂ (i : ι), edgeSet (f i)) ∩ SimpleGraph.edgeSet G
[PROOFSTEP]
simp [iInf]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
H₁ H₂ : Subgraph G
h : Disjoint H₁ H₂
⊢ SimpleGraph.Subgraph.edgeSet H₁ ⊓ SimpleGraph.Subgraph.edgeSet H₂ ≤ ⊥
[PROOFSTEP]
simpa using edgeSet_mono h.le_bot
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
⊢ ∀ {v w : W}, Relation.Map H.Adj (↑f) (↑f) v w → SimpleGraph.Adj G' v w
[PROOFSTEP]
rintro _ _ ⟨u, v, h, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
u v : V
h : Adj H u v
⊢ SimpleGraph.Adj G' (↑f u) (↑f v)
[PROOFSTEP]
exact f.map_rel (H.adj_sub h)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
⊢ ∀ {v w : W}, Relation.Map H.Adj (↑f) (↑f) v w → v ∈ ↑f '' H.verts
[PROOFSTEP]
rintro _ _ ⟨u, v, h, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
u v : V
h : Adj H u v
⊢ ↑f u ∈ ↑f '' H.verts
[PROOFSTEP]
exact Set.mem_image_of_mem _ (H.edge_vert h)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
⊢ Symmetric (Relation.Map H.Adj ↑f ↑f)
[PROOFSTEP]
rintro _ _ ⟨u, v, h, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
u v : V
h : Adj H u v
⊢ Relation.Map H.Adj (↑f) (↑f) (↑f v) (↑f u)
[PROOFSTEP]
exact ⟨v, u, H.symm h, rfl, rfl⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
⊢ Monotone (Subgraph.map f)
[PROOFSTEP]
intro H H' h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
⊢ Subgraph.map f H ≤ Subgraph.map f H'
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
⊢ (Subgraph.map f H).verts ⊆ (Subgraph.map f H').verts
[PROOFSTEP]
intro
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
a✝ : W
⊢ a✝ ∈ (Subgraph.map f H).verts → a✝ ∈ (Subgraph.map f H').verts
[PROOFSTEP]
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
a✝ : W
⊢ ∀ (x : V), x ∈ H.verts → ↑f x = a✝ → ∃ x, x ∈ H'.verts ∧ ↑f x = a✝
[PROOFSTEP]
rintro v hv rfl
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
v : V
hv : v ∈ H.verts
⊢ ∃ x, x ∈ H'.verts ∧ ↑f x = ↑f v
[PROOFSTEP]
exact ⟨_, h.1 hv, rfl⟩
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
⊢ ∀ ⦃v w : W⦄, Adj (Subgraph.map f H) v w → Adj (Subgraph.map f H') v w
[PROOFSTEP]
rintro _ _ ⟨u, v, ha, rfl, rfl⟩
[GOAL]
case right.intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
h : H ≤ H'
u v : V
ha : Adj H u v
⊢ Adj (Subgraph.map f H') (↑f u) (↑f v)
[PROOFSTEP]
exact ⟨_, _, h.2 ha, rfl, rfl⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ Subgraph.map f (H ⊔ H') = Subgraph.map f H ⊔ Subgraph.map f H'
[PROOFSTEP]
ext1
[GOAL]
case verts
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ (Subgraph.map f (H ⊔ H')).verts = (Subgraph.map f H ⊔ Subgraph.map f H').verts
[PROOFSTEP]
simp only [Set.image_union, map_verts, verts_sup]
[GOAL]
case Adj
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
⊢ (Subgraph.map f (H ⊔ H')).Adj = (Subgraph.map f H ⊔ Subgraph.map f H').Adj
[PROOFSTEP]
ext
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ Adj (Subgraph.map f (H ⊔ H')) x✝¹ x✝ ↔ Adj (Subgraph.map f H ⊔ Subgraph.map f H') x✝¹ x✝
[PROOFSTEP]
simp only [Relation.Map, map_Adj, sup_adj]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ (∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ↔
    (∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
[PROOFSTEP]
constructor
[GOAL]
case Adj.h.h.a.mp
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ (∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) →
    (∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
[PROOFSTEP]
rintro ⟨a, b, h | h, rfl, rfl⟩
[GOAL]
case Adj.h.h.a.mp.intro.intro.intro.inl.intro
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H a b
⊢ (∃ a_1 b_1, Adj H a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b) ∨ ∃ a_1 b_1, Adj H' a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
[PROOFSTEP]
exact Or.inl ⟨_, _, h, rfl, rfl⟩
[GOAL]
case Adj.h.h.a.mp.intro.intro.intro.inr.intro
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H' a b
⊢ (∃ a_1 b_1, Adj H a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b) ∨ ∃ a_1 b_1, Adj H' a_1 b_1 ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
[PROOFSTEP]
exact Or.inr ⟨_, _, h, rfl, rfl⟩
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a b : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
x✝¹ x✝ : W
⊢ ((∃ a b, Adj H a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ∨ ∃ a b, Adj H' a b ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) →
    ∃ a b, (Adj H a b ∨ Adj H' a b) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
[PROOFSTEP]
rintro (⟨a, b, h, rfl, rfl⟩ | ⟨a, b, h, rfl, rfl⟩)
[GOAL]
case Adj.h.h.a.mpr.inl.intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H a b
⊢ ∃ a_1 b_1, (Adj H a_1 b_1 ∨ Adj H' a_1 b_1) ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
[PROOFSTEP]
exact ⟨_, _, Or.inl h, rfl, rfl⟩
[GOAL]
case Adj.h.h.a.mpr.inr.intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G✝ : SimpleGraph V
G₁ G₂ : Subgraph G✝
a✝ b✝ : V
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G
a b : V
h : Adj H' a b
⊢ ∃ a_1 b_1, (Adj H a_1 b_1 ∨ Adj H' a_1 b_1) ∧ ↑f a_1 = ↑f a ∧ ↑f b_1 = ↑f b
[PROOFSTEP]
exact ⟨_, _, Or.inr h, rfl, rfl⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
⊢ Monotone (Subgraph.comap f)
[PROOFSTEP]
intro H H' h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ Subgraph.comap f H ≤ Subgraph.comap f H'
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts
[PROOFSTEP]
intro
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
a✝ : V
⊢ a✝ ∈ (Subgraph.comap f H).verts → a✝ ∈ (Subgraph.comap f H').verts
[PROOFSTEP]
simp only [comap_verts, Set.mem_preimage]
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
a✝ : V
⊢ ↑f a✝ ∈ H.verts → ↑f a✝ ∈ H'.verts
[PROOFSTEP]
apply h.1
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ ∀ ⦃v w : V⦄, Adj (Subgraph.comap f H) v w → Adj (Subgraph.comap f H') v w
[PROOFSTEP]
intro v w
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
⊢ Adj (Subgraph.comap f H) v w → Adj (Subgraph.comap f H') v w
[PROOFSTEP]
simp (config := { contextual := true }) only [comap_Adj, and_imp, true_and_iff]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
⊢ SimpleGraph.Adj G v w → Adj H (↑f v) (↑f w) → Adj H' (↑f v) (↑f w)
[PROOFSTEP]
intro
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
a✝ : SimpleGraph.Adj G v w
⊢ Adj H (↑f v) (↑f w) → Adj H' (↑f v) (↑f w)
[PROOFSTEP]
apply h.2
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'
[PROOFSTEP]
refine' ⟨fun h ↦ ⟨fun v hv ↦ _, fun v w hvw ↦ _⟩, fun h ↦ ⟨fun v ↦ _, fun v w ↦ _⟩⟩
[GOAL]
case refine'_1
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ v ∈ (Subgraph.comap f H').verts
[PROOFSTEP]
simp only [comap_verts, Set.mem_preimage]
[GOAL]
case refine'_1
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ ↑f v ∈ H'.verts
[PROOFSTEP]
exact h.1 ⟨v, hv, rfl⟩
[GOAL]
case refine'_2
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v w : V
hvw : Adj H v w
⊢ Adj (Subgraph.comap f H') v w
[PROOFSTEP]
simp only [H.adj_sub hvw, comap_Adj, true_and_iff]
[GOAL]
case refine'_2
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v w : V
hvw : Adj H v w
⊢ Adj H' (↑f v) (↑f w)
[PROOFSTEP]
exact h.2 ⟨v, w, hvw, rfl, rfl⟩
[GOAL]
case refine'_3
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts
[PROOFSTEP]
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
[GOAL]
case refine'_3
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v : W
⊢ ∀ (x : V), x ∈ H.verts → ↑f x = v → v ∈ H'.verts
[PROOFSTEP]
rintro w hw rfl
[GOAL]
case refine'_3
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
w : V
hw : w ∈ H.verts
⊢ ↑f w ∈ H'.verts
[PROOFSTEP]
exact h.1 hw
[GOAL]
case refine'_4
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v w : W
⊢ Adj (Subgraph.map f H) v w → Adj H' v w
[PROOFSTEP]
simp only [Relation.Map, map_Adj, forall_exists_index, and_imp]
[GOAL]
case refine'_4
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v w : W
⊢ ∀ (x x_1 : V), Adj H x x_1 → ↑f x = v → ↑f x_1 = w → Adj H' v w
[PROOFSTEP]
rintro u u' hu rfl rfl
[GOAL]
case refine'_4
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
u u' : V
hu : Adj H u u'
⊢ Adj H' (↑f u) (↑f u')
[PROOFSTEP]
exact (h.2 hu).2
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h : x ≤ y
⊢ Function.Injective ↑(inclusion h)
[PROOFSTEP]
intro v w h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h✝ : x ≤ y
v w : ↑x.verts
h : ↑(inclusion h✝) v = ↑(inclusion h✝) w
⊢ v = w
[PROOFSTEP]
rw [inclusion, FunLike.coe, Subtype.mk_eq_mk] at h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h✝ : x ≤ y
v w : ↑x.verts
h :
  ↑(RelHomClass.toFunLike.1
        { toFun := fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) },
          map_rel' :=
            (_ :
              ∀ {a b : ↑x.verts},
                SimpleGraph.Adj (Subgraph.coe x) a b →
                  Adj y ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) a)
                    ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) b)) }
        v) =
    ↑(RelHomClass.toFunLike.1
        { toFun := fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) },
          map_rel' :=
            (_ :
              ∀ {a b : ↑x.verts},
                SimpleGraph.Adj (Subgraph.coe x) a b →
                  Adj y ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) a)
                    ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) b)) }
        w)
⊢ v = w
[PROOFSTEP]
exact Subtype.ext h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝¹ : Fintype V
G' : Subgraph G
inst✝ : Fintype ↑G'.verts
h : IsSpanning G'
⊢ Finset.card (Set.toFinset G'.verts) = Fintype.card V
[PROOFSTEP]
simp only [isSpanning_iff.1 h, Set.toFinset_univ]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝¹ : Fintype V
G' : Subgraph G
inst✝ : Fintype ↑G'.verts
h : IsSpanning G'
⊢ Finset.card Finset.univ = Fintype.card V
[PROOFSTEP]
congr
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ Finset.card (Set.toFinset (neighborSet G' v)) = degree G' v
[PROOFSTEP]
rw [degree, Set.toFinset_card]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝¹ : Fintype ↑(neighborSet G' v)
inst✝ : Fintype ↑(SimpleGraph.neighborSet G v)
⊢ degree G' v ≤ SimpleGraph.degree G v
[PROOFSTEP]
rw [← card_neighborSet_eq_degree]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝¹ : Fintype ↑(neighborSet G' v)
inst✝ : Fintype ↑(SimpleGraph.neighborSet G v)
⊢ degree G' v ≤ Fintype.card ↑(SimpleGraph.neighborSet G v)
[PROOFSTEP]
exact Set.card_le_of_subset (G'.neighborSet_subset v)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : ↑G'.verts
inst✝¹ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.coe G') v)
inst✝ : Fintype ↑(neighborSet G' ↑v)
⊢ SimpleGraph.degree (Subgraph.coe G') v = degree G' ↑v
[PROOFSTEP]
rw [← card_neighborSet_eq_degree]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : ↑G'.verts
inst✝¹ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.coe G') v)
inst✝ : Fintype ↑(neighborSet G' ↑v)
⊢ Fintype.card ↑(SimpleGraph.neighborSet (Subgraph.coe G') v) = degree G' ↑v
[PROOFSTEP]
exact Fintype.card_congr (coeNeighborSetEquiv v)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝¹ : Fintype ↑(neighborSet G' v)
inst✝ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v)
⊢ SimpleGraph.degree (Subgraph.spanningCoe G') v = degree G' v
[PROOFSTEP]
rw [← card_neighborSet_eq_degree, Subgraph.degree]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝¹ : Fintype ↑(neighborSet G' v)
inst✝ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v)
⊢ Fintype.card ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v) = Fintype.card ↑(neighborSet G' v)
[PROOFSTEP]
congr!
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ degree G' v = 1 ↔ ∃! w, Adj G' v w
[PROOFSTEP]
rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ (∃! a, a ∈ Set.toFinset (neighborSet G' v)) ↔ ∃! w, Adj G' v w
[PROOFSTEP]
simp only [Set.mem_toFinset, mem_neighborSet]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
⊢ SimpleGraph.singletonSubgraph G v ≤ H ↔ v ∈ H.verts
[PROOFSTEP]
refine' ⟨fun h ↦ h.1 (Set.mem_singleton v), _⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
⊢ v ∈ H.verts → SimpleGraph.singletonSubgraph G v ≤ H
[PROOFSTEP]
intro h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ SimpleGraph.singletonSubgraph G v ≤ H
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ (SimpleGraph.singletonSubgraph G v).verts ⊆ H.verts
[PROOFSTEP]
rwa [singletonSubgraph_verts, Set.singleton_subset_iff]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, Subgraph.Adj (SimpleGraph.singletonSubgraph G v) v_1 w → Subgraph.Adj H v_1 w
[PROOFSTEP]
exact fun _ _ ↦ False.elim
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
⊢ Subgraph.map f (SimpleGraph.singletonSubgraph G v) = SimpleGraph.singletonSubgraph G' (↑f v)
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (SimpleGraph.singletonSubgraph G v)).verts ↔ x✝ ∈ (SimpleGraph.singletonSubgraph G' (↑f v)).verts
[PROOFSTEP]
simp only [Relation.Map, Subgraph.map_Adj, singletonSubgraph_Adj, Pi.bot_apply, exists_and_left, and_iff_left_iff_imp,
  IsEmpty.forall_iff, Subgraph.map_verts, singletonSubgraph_verts, Set.image_singleton]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ Subgraph.Adj (Subgraph.map f (SimpleGraph.singletonSubgraph G v)) x✝¹ x✝ ↔
    Subgraph.Adj (SimpleGraph.singletonSubgraph G' (↑f v)) x✝¹ x✝
[PROOFSTEP]
simp only [Relation.Map, Subgraph.map_Adj, singletonSubgraph_Adj, Pi.bot_apply, exists_and_left, and_iff_left_iff_imp,
  IsEmpty.forall_iff, Subgraph.map_verts, singletonSubgraph_verts, Set.image_singleton]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ ⊥ → ∃ x, ↑f x = x✝¹ ∧ ∃ x, ↑f x = x✝
[PROOFSTEP]
exact False.elim
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
⊢ H = SimpleGraph.singletonSubgraph G v ↔ H.verts = {v}
[PROOFSTEP]
refine' ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ _⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H = SimpleGraph.singletonSubgraph G v
⊢ H.verts = {v}
[PROOFSTEP]
rw [h, singletonSubgraph_verts]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
⊢ H = SimpleGraph.singletonSubgraph G v
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (SimpleGraph.singletonSubgraph G v).verts
[PROOFSTEP]
rw [h, singletonSubgraph_verts]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ Subgraph.Adj H x✝¹ x✝ ↔ Subgraph.Adj (SimpleGraph.singletonSubgraph G v) x✝¹ x✝
[PROOFSTEP]
simp only [Prop.bot_eq_false, singletonSubgraph_Adj, Pi.bot_apply, iff_false_iff]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ ¬Subgraph.Adj H x✝¹ x✝
[PROOFSTEP]
intro ha
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
⊢ False
[PROOFSTEP]
have ha1 := ha.fst_mem
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
⊢ False
[PROOFSTEP]
have ha2 := ha.snd_mem
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
ha2 : x✝ ∈ H.verts
⊢ False
[PROOFSTEP]
rw [h, Set.mem_singleton_iff] at ha1 ha2
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False
[PROOFSTEP]
subst_vars
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
x✝ : V
ha : Subgraph.Adj H x✝ x✝
h : H.verts = {x✝}
⊢ False
[PROOFSTEP]
exact ha.ne rfl
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ v ∈ (subgraphOfAdj G hvw).verts
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.edgeSet (subgraphOfAdj G hvw) = {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
[PROOFSTEP]
ext e
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
e : Sym2 V
⊢ e ∈ Subgraph.edgeSet (subgraphOfAdj G hvw) ↔ e ∈ {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
[PROOFSTEP]
refine' e.ind _
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
e : Sym2 V
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ Subgraph.edgeSet (subgraphOfAdj G hvw) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
[PROOFSTEP]
simp only [eq_comm, Set.mem_singleton_iff, Subgraph.mem_edgeSet, subgraphOfAdj_Adj, iff_self_iff, forall₂_true_iff]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
⊢ subgraphOfAdj G (_ : Adj G v w) ≤ H
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
⊢ (subgraphOfAdj G (_ : Adj G v w)).verts ⊆ H.verts
[PROOFSTEP]
intro x
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
x : V
⊢ x ∈ (subgraphOfAdj G (_ : Adj G v w)).verts → x ∈ H.verts
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case left.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
w : V
H : Subgraph G
x : V
h : Subgraph.Adj H x w
⊢ x ∈ H.verts
[PROOFSTEP]
simp [H.edge_vert h, H.edge_vert h.symm]
[GOAL]
case left.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
x : V
h : Subgraph.Adj H v x
⊢ x ∈ H.verts
[PROOFSTEP]
simp [H.edge_vert h, H.edge_vert h.symm]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
⊢ ∀ ⦃v_1 w_1 : V⦄, Subgraph.Adj (subgraphOfAdj G (_ : Adj G v w)) v_1 w_1 → Subgraph.Adj H v_1 w_1
[PROOFSTEP]
simp only [subgraphOfAdj_Adj, Quotient.eq, Sym2.rel_iff]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
⊢ ∀ ⦃v_1 w_1 : V⦄, v = v_1 ∧ w = w_1 ∨ v = w_1 ∧ w = v_1 → Subgraph.Adj H v_1 w_1
[PROOFSTEP]
rintro _ _ (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case right.inl.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
⊢ Subgraph.Adj H v w
[PROOFSTEP]
simp [h, h.symm]
[GOAL]
case right.inr.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
H : Subgraph G
h : Subgraph.Adj H v w
⊢ Subgraph.Adj H w v
[PROOFSTEP]
simp [h, h.symm]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ subgraphOfAdj G (_ : Adj G w v) = subgraphOfAdj G hvw
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
x✝ : V
⊢ x✝ ∈ (subgraphOfAdj G (_ : Adj G w v)).verts ↔ x✝ ∈ (subgraphOfAdj G hvw).verts
[PROOFSTEP]
simp [or_comm, and_comm]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
x✝¹ x✝ : V
⊢ Subgraph.Adj (subgraphOfAdj G (_ : Adj G w v)) x✝¹ x✝ ↔ Subgraph.Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
simp [or_comm, and_comm]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ Subgraph.map f (subgraphOfAdj G hvw) = subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (subgraphOfAdj G hvw)).verts ↔ x✝ ∈ (subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))).verts
[PROOFSTEP]
simp only [Subgraph.map_verts, subgraphOfAdj_verts, Set.mem_image, Set.mem_insert_iff, Set.mem_singleton_iff]
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝) ↔ x✝ = ↑f v ∨ x✝ = ↑f w
[PROOFSTEP]
constructor
[GOAL]
case verts.h.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝) → x✝ = ↑f v ∨ x✝ = ↑f w
[PROOFSTEP]
rintro ⟨u, rfl | rfl, rfl⟩
[GOAL]
case verts.h.mp.intro.intro.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
w u : V
hvw : Adj G u w
⊢ ↑f u = ↑f u ∨ ↑f u = ↑f w
[PROOFSTEP]
simp
[GOAL]
case verts.h.mp.intro.intro.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v u : V
hvw : Adj G v u
⊢ ↑f u = ↑f v ∨ ↑f u = ↑f u
[PROOFSTEP]
simp
[GOAL]
case verts.h.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ x✝ = ↑f v ∨ x✝ = ↑f w → ∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case verts.h.mpr.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ x, (x = v ∨ x = w) ∧ ↑f x = ↑f v
[PROOFSTEP]
use v
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = v ∨ v = w) ∧ ↑f v = ↑f v
[PROOFSTEP]
simp
[GOAL]
case verts.h.mpr.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ x, (x = v ∨ x = w) ∧ ↑f x = ↑f w
[PROOFSTEP]
use w
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (w = v ∨ w = w) ∧ ↑f w = ↑f w
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ Subgraph.Adj (Subgraph.map f (subgraphOfAdj G hvw)) x✝¹ x✝ ↔
    Subgraph.Adj (subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))) x✝¹ x✝
[PROOFSTEP]
simp only [Relation.Map, Subgraph.map_Adj, subgraphOfAdj_Adj, Quotient.eq, Sym2.rel_iff]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ (∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ↔ ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹
[PROOFSTEP]
constructor
[GOAL]
case Adj.h.h.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ (∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) → ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹
[PROOFSTEP]
rintro ⟨a, b, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl, rfl⟩
[GOAL]
case Adj.h.h.a.mp.intro.intro.intro.inl.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ↑f v = ↑f v ∧ ↑f w = ↑f w ∨ ↑f v = ↑f w ∧ ↑f w = ↑f v
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a.mp.intro.intro.intro.inr.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ↑f v = ↑f w ∧ ↑f w = ↑f v ∨ ↑f v = ↑f v ∧ ↑f w = ↑f w
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹ → ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case Adj.h.h.a.mpr.inl.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = ↑f v ∧ ↑f b = ↑f w
[PROOFSTEP]
use v, w
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ ↑f v = ↑f v ∧ ↑f w = ↑f w
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a.mpr.inr.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = ↑f w ∧ ↑f b = ↑f v
[PROOFSTEP]
use w, v
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = w ∧ w = v ∨ v = v ∧ w = w) ∧ ↑f w = ↑f w ∧ ↑f v = ↑f v
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) v = {w}
[PROOFSTEP]
ext u
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
⊢ u ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) v ↔ u ∈ {w}
[PROOFSTEP]
suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
this : w = u ↔ u = w
⊢ u ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) v ↔ u ∈ {w}
[PROOFSTEP]
simpa [hvw.ne.symm] using this
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
u : V
⊢ w = u ↔ u = w
[PROOFSTEP]
rw [eq_comm]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) w = {v}
[PROOFSTEP]
rw [subgraphOfAdj_symm hvw.symm]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G (_ : Adj G w v)) w = {v}
[PROOFSTEP]
exact neighborSet_fst_subgraphOfAdj hvw.symm
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v w : V
hvw : Adj G v w
hv : u ≠ v
hw : u ≠ w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = ∅
[PROOFSTEP]
ext
[GOAL]
case h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v w : V
hvw : Adj G v w
hv : u ≠ v
hw : u ≠ w
x✝ : V
⊢ x✝ ∈ Subgraph.neighborSet (subgraphOfAdj G hvw) u ↔ x✝ ∈ ∅
[PROOFSTEP]
simp [hv.symm, hw.symm]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
h✝¹ : u = v
h✝ : u = w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = {w} ∪ {v}
[PROOFSTEP]
subst_vars
[GOAL]
case neg
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
h✝¹ : u = v
h✝ : ¬u = w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = {w} ∪ ∅
[PROOFSTEP]
subst_vars
[GOAL]
case pos
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
h✝¹ : ¬u = v
h✝ : u = w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = ∅ ∪ {v}
[PROOFSTEP]
subst_vars
[GOAL]
case neg
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = ∅ ∪ ∅
[PROOFSTEP]
subst_vars
[GOAL]
case pos
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
w : V
hvw : Adj G w w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) w = {w} ∪ {w}
[PROOFSTEP]
simp [*]
[GOAL]
case neg
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
v w : V
hvw : Adj G v w
h✝ : ¬v = w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) v = {w} ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
v w : V
hvw : Adj G v w
h✝ : ¬w = v
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) w = ∅ ∪ {v}
[PROOFSTEP]
simp [*]
[GOAL]
case neg
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
inst✝ : DecidableEq V
u v w : V
hvw : Adj G v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ Subgraph.neighborSet (subgraphOfAdj G hvw) u = ∅ ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ SimpleGraph.singletonSubgraph G u ≤ subgraphOfAdj G h
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ (SimpleGraph.singletonSubgraph G u).verts ⊆ (subgraphOfAdj G h).verts
[PROOFSTEP]
simp [-Set.bot_eq_empty]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ ∀ ⦃v_1 w : V⦄, Subgraph.Adj (SimpleGraph.singletonSubgraph G u) v_1 w → Subgraph.Adj (subgraphOfAdj G h) v_1 w
[PROOFSTEP]
simp [-Set.bot_eq_empty]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ ∀ ⦃v_1 w : V⦄, ⊥ → u = v_1 ∧ v = w ∨ u = w ∧ v = v_1
[PROOFSTEP]
exact fun _ _ ↦ False.elim
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ SimpleGraph.singletonSubgraph G v ≤ subgraphOfAdj G h
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ (SimpleGraph.singletonSubgraph G v).verts ⊆ (subgraphOfAdj G h).verts
[PROOFSTEP]
simp [-Set.bot_eq_empty]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ ∀ ⦃v_1 w : V⦄, Subgraph.Adj (SimpleGraph.singletonSubgraph G v) v_1 w → Subgraph.Adj (subgraphOfAdj G h) v_1 w
[PROOFSTEP]
simp [-Set.bot_eq_empty]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ ∀ ⦃v_1 w : V⦄, ⊥ → u = v_1 ∧ v = w ∨ u = w ∧ v = v_1
[PROOFSTEP]
exact fun _ _ ↦ False.elim
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
v w : V
⊢ Adj (Subgraph.coeSubgraph G'') v w ↔ ∃ hv hw, Adj G'' { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
simp [Relation.Map]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝¹ x✝ : ↑G'.verts
⊢ Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x✝¹ x✝ ↔ Adj G'' x✝¹ x✝
[PROOFSTEP]
rw [restrict_Adj, coeSubgraph_Adj]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝¹ x✝ : ↑G'.verts
⊢ (Adj G' ↑x✝¹ ↑x✝ ∧ ∃ hv hw, Adj G'' { val := ↑x✝¹, property := hv } { val := ↑x✝, property := hw }) ↔ Adj G'' x✝¹ x✝
[PROOFSTEP]
simpa using G''.adj_sub
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H : Subgraph G
H' : Subgraph (Subgraph.coe H)
⊢ Subgraph.coeSubgraph H' ≤ H
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H : Subgraph G
H' : Subgraph (Subgraph.coe H)
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts
[PROOFSTEP]
simp
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H : Subgraph G
H' : Subgraph (Subgraph.coe H)
⊢ ∀ ⦃v w : V⦄, Adj (Subgraph.coeSubgraph H') v w → Adj H v w
[PROOFSTEP]
rintro v w ⟨_, _, h, rfl, rfl⟩
[GOAL]
case right.intro.intro.intro.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H : Subgraph G
H' : Subgraph (Subgraph.coe H)
w✝¹ w✝ : ↑H.verts
h : Adj H' w✝¹ w✝
⊢ Adj H (↑(Subgraph.hom H) w✝¹) (↑(Subgraph.hom H) w✝)
[PROOFSTEP]
exact H'.adj_sub h
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H H' : Subgraph G
⊢ Subgraph.coeSubgraph (Subgraph.restrict H') = H ⊓ H'
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H H' : Subgraph G
x✝ : V
⊢ x✝ ∈ (Subgraph.coeSubgraph (Subgraph.restrict H')).verts ↔ x✝ ∈ (H ⊓ H').verts
[PROOFSTEP]
simp [and_comm]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H H' : Subgraph G
x✝¹ x✝ : V
⊢ Adj (Subgraph.coeSubgraph (Subgraph.restrict H')) x✝¹ x✝ ↔ Adj (H ⊓ H') x✝¹ x✝
[PROOFSTEP]
simp_rw [coeSubgraph_Adj, restrict_Adj]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H H' : Subgraph G
x✝¹ x✝ : V
⊢ (∃ h h, Adj H x✝¹ x✝ ∧ Adj H' x✝¹ x✝) ↔ Adj (H ⊓ H') x✝¹ x✝
[PROOFSTEP]
simp only [exists_and_left, exists_prop, ge_iff_le, inf_adj, and_congr_right_iff]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H H' : Subgraph G
x✝¹ x✝ : V
⊢ Adj H x✝¹ x✝ → (x✝ ∈ H.verts ∧ x✝¹ ∈ H.verts ∧ Adj H' x✝¹ x✝ ↔ Adj H' x✝¹ x✝)
[PROOFSTEP]
intro h
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
H H' : Subgraph G
x✝¹ x✝ : V
h : Adj H x✝¹ x✝
⊢ x✝ ∈ H.verts ∧ x✝¹ ∈ H.verts ∧ Adj H' x✝¹ x✝ ↔ Adj H' x✝¹ x✝
[PROOFSTEP]
simp [H.edge_vert h, H.edge_vert h.symm]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
a b : V
⊢ (G'.Adj \ Sym2.ToRel s) a b → (G'.Adj \ Sym2.ToRel s) b a
[PROOFSTEP]
simp [G'.adj_comm, Sym2.eq_swap]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
⊢ deleteEdges (deleteEdges G' s) s' = deleteEdges G' (s ∪ s')
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (deleteEdges (deleteEdges G' s) s').verts ↔ x✝ ∈ (deleteEdges G' (s ∪ s')).verts
[PROOFSTEP]
simp [and_assoc, not_or]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges (deleteEdges G' s) s') x✝¹ x✝ ↔ Adj (deleteEdges G' (s ∪ s')) x✝¹ x✝
[PROOFSTEP]
simp [and_assoc, not_or]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ deleteEdges G' ∅ = G'
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (deleteEdges G' ∅).verts ↔ x✝ ∈ G'.verts
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G' ∅) x✝¹ x✝ ↔ Adj G' x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ SimpleGraph.deleteEdges (Subgraph.spanningCoe G') s = Subgraph.spanningCoe (deleteEdges G' s)
[PROOFSTEP]
ext
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.spanningCoe G') s) x✝¹ x✝ ↔
    SimpleGraph.Adj (Subgraph.spanningCoe (deleteEdges G' s)) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
⊢ SimpleGraph.deleteEdges (Subgraph.coe G') s = Subgraph.coe (deleteEdges G' (Sym2.map Subtype.val '' s))
[PROOFSTEP]
ext ⟨v, hv⟩ ⟨w, hw⟩
[GOAL]
case Adj.h.mk.h.mk.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.coe G') s) { val := v, property := hv }
      { val := w, property := hw } ↔
    SimpleGraph.Adj (Subgraph.coe (deleteEdges G' (Sym2.map Subtype.val '' s))) { val := v, property := hv }
      { val := w, property := hw }
[PROOFSTEP]
simp only [SimpleGraph.deleteEdges_adj, coe_Adj, deleteEdges_adj, Set.mem_image, not_exists, not_and,
  and_congr_right_iff]
[GOAL]
case Adj.h.mk.h.mk.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ Adj G' v w →
    (¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s ↔
      ∀ (x : Sym2 ↑G'.verts), x ∈ s → ¬Sym2.map Subtype.val x = Quotient.mk (Sym2.Rel.setoid V) (v, w))
[PROOFSTEP]
intro
[GOAL]
case Adj.h.mk.h.mk.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
⊢ ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s ↔
    ∀ (x : Sym2 ↑G'.verts), x ∈ s → ¬Sym2.map Subtype.val x = Quotient.mk (Sym2.Rel.setoid V) (v, w)
[PROOFSTEP]
constructor
[GOAL]
case Adj.h.mk.h.mk.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
⊢ ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s →
    ∀ (x : Sym2 ↑G'.verts), x ∈ s → ¬Sym2.map Subtype.val x = Quotient.mk (Sym2.Rel.setoid V) (v, w)
[PROOFSTEP]
intro hs
[GOAL]
case Adj.h.mk.h.mk.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
⊢ ∀ (x : Sym2 ↑G'.verts), x ∈ s → ¬Sym2.map Subtype.val x = Quotient.mk (Sym2.Rel.setoid V) (v, w)
[PROOFSTEP]
refine' Sym2.ind _
[GOAL]
case Adj.h.mk.h.mk.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
⊢ ∀ (x y : ↑G'.verts),
    Quotient.mk (Sym2.Rel.setoid ↑G'.verts) (x, y) ∈ s →
      ¬Sym2.map Subtype.val (Quotient.mk (Sym2.Rel.setoid ↑G'.verts) (x, y)) = Quotient.mk (Sym2.Rel.setoid V) (v, w)
[PROOFSTEP]
rintro ⟨v', hv'⟩ ⟨w', hw'⟩
[GOAL]
case Adj.h.mk.h.mk.a.mp.mk.mk
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v', property := hv' }, { val := w', property := hw' }) ∈ s →
    ¬Sym2.map Subtype.val
          (Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v', property := hv' }, { val := w', property := hw' })) =
        Quotient.mk (Sym2.Rel.setoid V) (v, w)
[PROOFSTEP]
simp only [Sym2.map_pair_eq, Quotient.eq]
[GOAL]
case Adj.h.mk.h.mk.a.mp.mk.mk
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v', property := hv' }, { val := w', property := hw' }) ∈ s →
    ¬(v', w') ≈ (v, w)
[PROOFSTEP]
contrapose!
[GOAL]
case Adj.h.mk.h.mk.a.mp.mk.mk
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ (v', w') ≈ (v, w) →
    ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v', property := hv' }, { val := w', property := hw' }) ∈ s
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case Adj.h.mk.h.mk.a.mp.mk.mk.refl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
hv' : v ∈ G'.verts
hw' : w ∈ G'.verts
⊢ ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv' }, { val := w, property := hw' }) ∈ s
[PROOFSTEP]
simpa only [Sym2.eq_swap]
[GOAL]
case Adj.h.mk.h.mk.a.mp.mk.mk.swap
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
hs : ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
hw' : v ∈ G'.verts
hv' : w ∈ G'.verts
⊢ ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := w, property := hv' }, { val := v, property := hw' }) ∈ s
[PROOFSTEP]
simpa only [Sym2.eq_swap]
[GOAL]
case Adj.h.mk.h.mk.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
⊢ (∀ (x : Sym2 ↑G'.verts), x ∈ s → ¬Sym2.map Subtype.val x = Quotient.mk (Sym2.Rel.setoid V) (v, w)) →
    ¬Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
[PROOFSTEP]
intro h' hs
[GOAL]
case Adj.h.mk.h.mk.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ : Set (Sym2 V)
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : Adj G' v w
h' : ∀ (x : Sym2 ↑G'.verts), x ∈ s → ¬Sym2.map Subtype.val x = Quotient.mk (Sym2.Rel.setoid V) (v, w)
hs : Quotient.mk (Sym2.Rel.setoid ↑G'.verts) ({ val := v, property := hv }, { val := w, property := hw }) ∈ s
⊢ False
[PROOFSTEP]
exact h' _ hs rfl
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s : Set (Sym2 V)
⊢ Subgraph.coe (deleteEdges G' s) = SimpleGraph.deleteEdges (Subgraph.coe G') (Sym2.map Subtype.val ⁻¹' s)
[PROOFSTEP]
ext ⟨v, hv⟩ ⟨w, hw⟩
[GOAL]
case Adj.h.mk.h.mk.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s : Set (Sym2 V)
v : V
hv : v ∈ (deleteEdges G' s).verts
w : V
hw : w ∈ (deleteEdges G' s).verts
⊢ SimpleGraph.Adj (Subgraph.coe (deleteEdges G' s)) { val := v, property := hv } { val := w, property := hw } ↔
    SimpleGraph.Adj (SimpleGraph.deleteEdges (Subgraph.coe G') (Sym2.map Subtype.val ⁻¹' s))
      { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ deleteEdges G' s ≤ G'
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ (deleteEdges G' s).verts ⊆ G'.verts
[PROOFSTEP]
simp (config := { contextual := true }) [subset_rfl]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ ∀ ⦃v w : V⦄, Adj (deleteEdges G' s) v w → Adj G' v w
[PROOFSTEP]
simp (config := { contextual := true }) [subset_rfl]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ deleteEdges G' s' ≤ deleteEdges G' s
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ (deleteEdges G' s').verts ⊆ (deleteEdges G' s).verts
[PROOFSTEP]
simp (config := { contextual := true }) only [deleteEdges_verts, deleteEdges_adj, true_and_iff, and_imp, subset_rfl]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj (deleteEdges G' s') v w → Adj (deleteEdges G' s) v w
[PROOFSTEP]
simp (config := { contextual := true }) only [deleteEdges_verts, deleteEdges_adj, true_and_iff, and_imp, subset_rfl]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj G' v w → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s' → ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s
[PROOFSTEP]
exact fun _ _ _ hs' hs ↦ hs' (h hs)
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ deleteEdges G' (edgeSet G' ∩ s) = deleteEdges G' s
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (deleteEdges G' (edgeSet G' ∩ s)).verts ↔ x✝ ∈ (deleteEdges G' s).verts
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G' (edgeSet G' ∩ s)) x✝¹ x✝ ↔ Adj (deleteEdges G' s) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ deleteEdges G' (s ∩ edgeSet G') = deleteEdges G' s
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (deleteEdges G' (s ∩ edgeSet G')).verts ↔ x✝ ∈ (deleteEdges G' s).verts
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G' (s ∩ edgeSet G')) x✝¹ x✝ ↔ Adj (deleteEdges G' s) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ Subgraph.coe (deleteEdges G' s) ≤ Subgraph.coe G'
[PROOFSTEP]
intro v w
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
v w : ↑(deleteEdges G' s).verts
⊢ SimpleGraph.Adj (Subgraph.coe (deleteEdges G' s)) v w → SimpleGraph.Adj (Subgraph.coe G') v w
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
s : Set V
⊢ SimpleGraph.induce s G = Subgraph.coe (induce ⊤ s)
[PROOFSTEP]
ext
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
s : Set V
x✝¹ x✝ : ↑s
⊢ SimpleGraph.Adj (SimpleGraph.induce s G) x✝¹ x✝ ↔ SimpleGraph.Adj (Subgraph.coe (induce ⊤ s)) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ induce G' s ≤ induce G'' s'
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (induce G' s).verts ⊆ (induce G'' s').verts
[PROOFSTEP]
simp [hs]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj (induce G' s) v w → Adj (induce G'' s') v w
[PROOFSTEP]
simp (config := { contextual := true }) only [induce_Adj, true_and_iff, and_imp]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → Adj G' v w → v ∈ s' ∧ w ∈ s' ∧ Adj G'' v w
[PROOFSTEP]
intro v w hv hw ha
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : Adj G' v w
⊢ v ∈ s' ∧ w ∈ s' ∧ Adj G'' v w
[PROOFSTEP]
exact ⟨hs hv, hs hw, hg.2 ha⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ induce G' ∅ = ⊥
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝ : V
⊢ x✝ ∈ (induce G' ∅).verts ↔ x✝ ∈ ⊥.verts
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj (induce G' ∅) x✝¹ x✝ ↔ Adj ⊥ x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ induce G' G'.verts = G'
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝ : V
⊢ x✝ ∈ (induce G' G'.verts).verts ↔ x✝ ∈ G'.verts
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj (induce G' G'.verts) x✝¹ x✝ ↔ Adj G' x✝¹ x✝
[PROOFSTEP]
constructor
[GOAL]
case Adj.h.h.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj (induce G' G'.verts) x✝¹ x✝ → Adj G' x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) only [induce_Adj, imp_true_iff, and_true_iff]
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj G' x✝¹ x✝ → Adj (induce G' G'.verts) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) only [induce_Adj, imp_true_iff, and_true_iff]
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj G' x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts
[PROOFSTEP]
exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ induce G' s ⊔ induce G' s' ≤ induce G' (s ∪ s')
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ (induce G' s ⊔ induce G' s').verts ⊆ (induce G' (s ∪ s')).verts
[PROOFSTEP]
simp only [verts_sup, induce_verts, Set.Subset.rfl]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ ∀ ⦃v w : V⦄, Adj (induce G' s ⊔ induce G' s') v w → Adj (induce G' (s ∪ s')) v w
[PROOFSTEP]
simp only [sup_adj, induce_Adj, Set.mem_union]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ ∀ ⦃v w : V⦄,
    v ∈ s ∧ w ∈ s ∧ Adj G' v w ∨ v ∈ s' ∧ w ∈ s' ∧ Adj G' v w → (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ Adj G' v w
[PROOFSTEP]
rintro v w (h | h)
[GOAL]
case right.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
h : v ∈ s ∧ w ∈ s ∧ Adj G' v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ Adj G' v w
[PROOFSTEP]
simp [h]
[GOAL]
case right.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
h : v ∈ s' ∧ w ∈ s' ∧ Adj G' v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ Adj G' v w
[PROOFSTEP]
simp [h]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ induce G' s ≤ induce G' (s ∪ s')
[PROOFSTEP]
exact (sup_le_iff.mp le_induce_union).1
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ induce G' s' ≤ induce G' (s ∪ s')
[PROOFSTEP]
exact (sup_le_iff.mp le_induce_union).2
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v : V
⊢ SimpleGraph.singletonSubgraph G v = induce ⊤ {v}
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v x✝ : V
⊢ x✝ ∈ (SimpleGraph.singletonSubgraph G v).verts ↔ x✝ ∈ (induce ⊤ {v}).verts
[PROOFSTEP]
simp (config := { contextual := true }) [-Set.bot_eq_empty, Prop.bot_eq_false]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v x✝¹ x✝ : V
⊢ Adj (SimpleGraph.singletonSubgraph G v) x✝¹ x✝ ↔ Adj (induce ⊤ {v}) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) [-Set.bot_eq_empty, Prop.bot_eq_false]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
⊢ subgraphOfAdj G hvw = induce ⊤ {v, w}
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝ : V
⊢ x✝ ∈ (subgraphOfAdj G hvw).verts ↔ x✝ ∈ (induce ⊤ {v, w}).verts
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝ ↔ Adj (induce ⊤ {v, w}) x✝¹ x✝
[PROOFSTEP]
constructor
[GOAL]
case Adj.h.h.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝ → Adj (induce ⊤ {v, w}) x✝¹ x✝
[PROOFSTEP]
intro h
[GOAL]
case Adj.h.h.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : Adj (subgraphOfAdj G hvw) x✝¹ x✝
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝
[PROOFSTEP]
simp only [subgraphOfAdj_Adj, Quotient.eq, Sym2.rel_iff] at h
[GOAL]
case Adj.h.h.a.mp
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : v = x✝¹ ∧ w = x✝ ∨ v = x✝ ∧ w = x✝¹
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h
[GOAL]
case Adj.h.h.a.mp.inl.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
⊢ Adj (induce ⊤ {v, w}) v w
[PROOFSTEP]
simp [hvw, hvw.symm]
[GOAL]
case Adj.h.h.a.mp.inr.intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
⊢ Adj (induce ⊤ {v, w}) w v
[PROOFSTEP]
simp [hvw, hvw.symm]
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝ → Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
intro h
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : Adj (induce ⊤ {v, w}) x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
simp only [induce_Adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h
[GOAL]
case Adj.h.h.a.mpr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ SimpleGraph.Adj G x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h
[GOAL]
case Adj.h.h.a.mpr.intro.inl.intro.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
w x✝ : V
hvw : SimpleGraph.Adj G x✝ w
ha : SimpleGraph.Adj G x✝ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝ x✝
[PROOFSTEP]
first
| exact (ha.ne rfl).elim
| simp
[GOAL]
case Adj.h.h.a.mpr.intro.inl.intro.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
w x✝ : V
hvw : SimpleGraph.Adj G x✝ w
ha : SimpleGraph.Adj G x✝ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝ x✝
[PROOFSTEP]
exact (ha.ne rfl).elim
[GOAL]
case Adj.h.h.a.mpr.intro.inl.intro.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha hvw : SimpleGraph.Adj G x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
first
| exact (ha.ne rfl).elim
| simp
[GOAL]
case Adj.h.h.a.mpr.intro.inl.intro.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha hvw : SimpleGraph.Adj G x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
exact (ha.ne rfl).elim
[GOAL]
case Adj.h.h.a.mpr.intro.inl.intro.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha hvw : SimpleGraph.Adj G x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a.mpr.intro.inr.intro.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha : SimpleGraph.Adj G x✝¹ x✝
hvw : SimpleGraph.Adj G x✝ x✝¹
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
first
| exact (ha.ne rfl).elim
| simp
[GOAL]
case Adj.h.h.a.mpr.intro.inr.intro.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha : SimpleGraph.Adj G x✝¹ x✝
hvw : SimpleGraph.Adj G x✝ x✝¹
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
exact (ha.ne rfl).elim
[GOAL]
case Adj.h.h.a.mpr.intro.inr.intro.inl
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha : SimpleGraph.Adj G x✝¹ x✝
hvw : SimpleGraph.Adj G x✝ x✝¹
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
case Adj.h.h.a.mpr.intro.inr.intro.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v x✝ : V
hvw : SimpleGraph.Adj G v x✝
ha : SimpleGraph.Adj G x✝ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝ x✝
[PROOFSTEP]
first
| exact (ha.ne rfl).elim
| simp
[GOAL]
case Adj.h.h.a.mpr.intro.inr.intro.inr
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v x✝ : V
hvw : SimpleGraph.Adj G v x✝
ha : SimpleGraph.Adj G x✝ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝ x✝
[PROOFSTEP]
exact (ha.ne rfl).elim
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
u v : V
⊢ Adj (deleteVerts G' s) u v ↔ u ∈ G'.verts ∧ ¬u ∈ s ∧ v ∈ G'.verts ∧ ¬v ∈ s ∧ Adj G' u v
[PROOFSTEP]
simp [and_assoc]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set V
⊢ deleteVerts (deleteVerts G' s) s' = deleteVerts G' (s ∪ s')
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set V
x✝ : V
⊢ x✝ ∈ (deleteVerts (deleteVerts G' s) s').verts ↔ x✝ ∈ (deleteVerts G' (s ∪ s')).verts
[PROOFSTEP]
simp (config := { contextual := true }) [not_or, and_assoc]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s✝ s s' : Set V
x✝¹ x✝ : V
⊢ Adj (deleteVerts (deleteVerts G' s) s') x✝¹ x✝ ↔ Adj (deleteVerts G' (s ∪ s')) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) [not_or, and_assoc]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
⊢ deleteVerts G' ∅ = G'
[PROOFSTEP]
simp [deleteVerts]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
⊢ deleteVerts G' s ≤ G'
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
⊢ (deleteVerts G' s).verts ⊆ G'.verts
[PROOFSTEP]
simp [Set.diff_subset]
[GOAL]
case right
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
⊢ ∀ ⦃v w : V⦄, Adj (deleteVerts G' s) v w → Adj G' v w
[PROOFSTEP]
simp [Set.diff_subset]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
⊢ deleteVerts G' (G'.verts ∩ s) = deleteVerts G' s
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
x✝ : V
⊢ x✝ ∈ (deleteVerts G' (G'.verts ∩ s)).verts ↔ x✝ ∈ (deleteVerts G' s).verts
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
x✝¹ x✝ : V
⊢ Adj (deleteVerts G' (G'.verts ∩ s)) x✝¹ x✝ ↔ Adj (deleteVerts G' s) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
⊢ deleteVerts G' (s ∩ G'.verts) = deleteVerts G' s
[PROOFSTEP]
ext
[GOAL]
case verts.h
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
x✝ : V
⊢ x✝ ∈ (deleteVerts G' (s ∩ G'.verts)).verts ↔ x✝ ∈ (deleteVerts G' s).verts
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]
[GOAL]
case Adj.h.h.a
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set V
x✝¹ x✝ : V
⊢ Adj (deleteVerts G' (s ∩ G'.verts)) x✝¹ x✝ ↔ Adj (deleteVerts G' s) x✝¹ x✝
[PROOFSTEP]
simp (config := { contextual := true }) [imp_false]


[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = if e ∈ incidenceSet G a then 1 else 0
[PROOFSTEP]
unfold incMatrix Set.indicator
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ (if e ∈ incidenceSet G a then OfNat.ofNat 1 e else 0) = if e ∈ incidenceSet G a then 1 else 0
[PROOFSTEP]
simp only [Pi.one_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = Set.indicator (incidenceSet G a ∩ incidenceSet G b) 1 e
[PROOFSTEP]
classical simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one, Set.mem_inter_iff]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = Set.indicator (incidenceSet G a ∩ incidenceSet G b) 1 e
[PROOFSTEP]
simp only [incMatrix, Set.indicator_apply, ← ite_and_mul_zero, Pi.one_apply, mul_one, Set.mem_inter_iff]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ incMatrix R G a e * incMatrix R G b e = 0
[PROOFSTEP]
rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_not_mem]
[GOAL]
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ incidenceSet G a ∩ incidenceSet G b
[PROOFSTEP]
rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]
[GOAL]
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬Adj G a b
⊢ ¬e ∈ ∅
[PROOFSTEP]
exact Set.not_mem_empty e
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
h : ¬e ∈ incidenceSet G a
⊢ incMatrix R G a e = 0
[PROOFSTEP]
rw [incMatrix_apply, Set.indicator_of_not_mem h]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
h : e ∈ incidenceSet G a
⊢ incMatrix R G a e = 1
[PROOFSTEP]
rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 0 ↔ ¬e ∈ incidenceSet G a
[PROOFSTEP]
simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ incidenceSet G a
[PROOFSTEP]
unfold incMatrix Set.indicator
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then OfNat.ofNat 1 e else 0) = 1 ↔ e ∈ incidenceSet G a
[PROOFSTEP]
simp only [Pi.one_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1 ↔ e ∈ incidenceSet G a
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1 → e ∈ incidenceSet G a
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ e ∈ incidenceSet G a → (if e ∈ incidenceSet G a then 1 else 0) = 1
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : (if e ∈ incidenceSet G a then 1 else 0) = 1
⊢ e ∈ incidenceSet G a
[PROOFSTEP]
split at h
[GOAL]
case mp.inl
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h✝ : e ∈ incidenceSet G a
h : 1 = 1
⊢ e ∈ incidenceSet G a
[PROOFSTEP]
simp_all only [zero_ne_one]
[GOAL]
case mp.inr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h✝ : ¬e ∈ incidenceSet G a
h : 0 = 1
⊢ e ∈ incidenceSet G a
[PROOFSTEP]
simp_all only [zero_ne_one]
[GOAL]
case mpr
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
h : e ∈ incidenceSet G a
⊢ (if e ∈ incidenceSet G a then 1 else 0) = 1
[PROOFSTEP]
simp_all only [ite_true]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ ∑ e : Sym2 α, incMatrix R G a e = ↑(degree G a)
[PROOFSTEP]
simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(degree G a)
[PROOFSTEP]
rw [← sum_incMatrix_apply]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e
[PROOFSTEP]
simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ (∑ x : Sym2 α, if x ∈ incidenceSet G a then if x ∈ incidenceSet G a then 1 else 0 else 0) =
    ∑ x : Sym2 α, if x ∈ incidenceSet G a then 1 else 0
[PROOFSTEP]
simp_all only [ite_true, sum_boole]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ e ∈ edgeSet G → ∑ a : α, incMatrix R G a e = 2
[PROOFSTEP]
classical
refine' e.ind _
intro a b h
rw [mem_edgeSet] at h
rw [← Nat.cast_two, ← card_doubleton h.ne]
simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h, true_and_iff]
congr 2
ext e
simp only [mem_filter, mem_univ, true_and_iff, mem_insert, mem_singleton]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ e ∈ edgeSet G → ∑ a : α, incMatrix R G a e = 2
[PROOFSTEP]
refine' e.ind _
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a b : α
e : Sym2 α
⊢ ∀ (x y : α),
    Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G → ∑ a : α, incMatrix R G a (Quotient.mk (Rel.setoid α) (x, y)) = 2
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) ∈ edgeSet G
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = 2
[PROOFSTEP]
rw [mem_edgeSet] at h
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = 2
[PROOFSTEP]
rw [← Nat.cast_two, ← card_doubleton h.ne]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ∑ a_1 : α, incMatrix R G a_1 (Quotient.mk (Rel.setoid α) (a, b)) = ↑(card {a, b})
[PROOFSTEP]
simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h, true_and_iff]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ ↑(card (filter (fun x => x = a ∨ x = b) univ)) = ↑(card {a, b})
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_s
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e : Sym2 α
a b : α
h : Adj G a b
⊢ filter (fun x => x = a ∨ x = b) univ = {a, b}
[PROOFSTEP]
ext e
[GOAL]
case e_a.e_s.a
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : NonAssocSemiring R
a✝ b✝ : α
e✝ : Sym2 α
a b : α
h : Adj G a b
e : α
⊢ e ∈ filter (fun x => x = a ∨ x = b) univ ↔ e ∈ {a, b}
[PROOFSTEP]
simp only [mem_filter, mem_univ, true_and_iff, mem_insert, mem_singleton]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ((incMatrix R G)ᵀ * incMatrix R G) e e = if e ∈ edgeSet G then 2 else 0
[PROOFSTEP]
classical
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ← ite_and_mul_zero, one_mul, sum_boole, and_self_iff]
split_ifs with h
· revert h
  refine' e.ind _
  intro v w h
  rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
  simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h]
  congr 2
  ext u
  simp
· revert h
  refine' e.ind _
  intro v w h
  simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ((incMatrix R G)ᵀ * incMatrix R G) e e = if e ∈ edgeSet G then 2 else 0
[PROOFSTEP]
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ← ite_and_mul_zero, one_mul, sum_boole, and_self_iff]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = if e ∈ edgeSet G then 2 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
h : e ∈ edgeSet G
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 2
[PROOFSTEP]
revert h
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ e ∈ edgeSet G → ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 2
[PROOFSTEP]
refine' e.ind _
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : α),
    Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G →
      ↑(card (filter (fun x_1 => Quotient.mk (Rel.setoid α) (x, y) ∈ incidenceSet G x_1) univ)) = 2
[PROOFSTEP]
intro v w h
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) = 2
[PROOFSTEP]
rw [← Nat.cast_two, ← card_doubleton (G.ne_of_adj h)]
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) =
    ↑(card {(v, w).fst, (v, w).snd})
[PROOFSTEP]
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h]
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => x = v ∨ x = w) univ)) = ↑(card {v, w})
[PROOFSTEP]
congr 2
[GOAL]
case pos.e_a.e_s
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ filter (fun x => x = v ∨ x = w) univ = {v, w}
[PROOFSTEP]
ext u
[GOAL]
case pos.e_a.e_s.a
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
u : α
⊢ u ∈ filter (fun x => x = v ∨ x = w) univ ↔ u ∈ {v, w}
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
h : ¬e ∈ edgeSet G
⊢ ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 0
[PROOFSTEP]
revert h
[GOAL]
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ¬e ∈ edgeSet G → ↑(card (filter (fun x => e ∈ incidenceSet G x) univ)) = 0
[PROOFSTEP]
refine' e.ind _
[GOAL]
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : α),
    ¬Quotient.mk (Rel.setoid α) (x, y) ∈ edgeSet G →
      ↑(card (filter (fun x_1 => Quotient.mk (Rel.setoid α) (x, y) ∈ incidenceSet G x_1) univ)) = 0
[PROOFSTEP]
intro v w h
[GOAL]
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝ : DecidableRel G.Adj
v w : α
h : ¬Quotient.mk (Rel.setoid α) (v, w) ∈ edgeSet G
⊢ ↑(card (filter (fun x => Quotient.mk (Rel.setoid α) (v, w) ∈ incidenceSet G x) univ)) = 0
[PROOFSTEP]
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
[PROOFSTEP]
classical
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply, Set.indicator_apply,
  Pi.one_apply, sum_boole]
convert @Nat.cast_one R _
convert card_singleton ⟦(a, b)⟧
rw [← coe_eq_singleton, coe_filter_univ]
exact G.incidenceSet_inter_incidenceSet_of_adj h
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
[PROOFSTEP]
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply, Set.indicator_apply,
  Pi.one_apply, sum_boole]
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ ↑(card (filter (fun x => x ∈ incidenceSet G a ∩ incidenceSet G b) univ)) = 1
[PROOFSTEP]
convert @Nat.cast_one R _
[GOAL]
case h.e'_2.h.e'_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
⊢ card (filter (fun x => x ∈ incidenceSet G a ∩ incidenceSet G b) univ) = 1
[PROOFSTEP]
convert card_singleton ⟦(a, b)⟧
[GOAL]
case h.e'_2.h.e'_2.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
e_1✝ : Sym2 α = Quotient (Rel.setoid α)
⊢ filter (fun x => x ∈ incidenceSet G a ∩ incidenceSet G b) univ = {Quotient.mk (Rel.setoid α) (a, b)}
[PROOFSTEP]
rw [← coe_eq_singleton, coe_filter_univ]
[GOAL]
case h.e'_2.h.e'_2.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
e : Sym2 α
h : Adj G a b
e_1✝ : Sym2 α = Quotient (Rel.setoid α)
⊢ {x | x ∈ incidenceSet G a ∩ incidenceSet G b} = {Quotient.mk (Rel.setoid α) (a, b)}
[PROOFSTEP]
exact G.incidenceSet_inter_incidenceSet_of_adj h
[GOAL]
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ incMatrix R G * (incMatrix R G)ᵀ = fun a b => if a = b then ↑(degree G a) else if Adj G a b then 1 else 0
[PROOFSTEP]
ext a b
[GOAL]
case a.h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then ↑(degree G a) else if Adj G a b then 1 else 0
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(degree G a)
[PROOFSTEP]
subst b
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(degree G a)
[PROOFSTEP]
rename Semiring R => sr
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
sr : Semiring R
a✝ b : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(degree G a)
[PROOFSTEP]
convert @incMatrix_mul_transpose_diag _ _ _ _ sr.toNonAssocSemiring _ _ _
[GOAL]
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : Adj G a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
[PROOFSTEP]
exact G.incMatrix_mul_transpose_apply_of_adj h'
[GOAL]
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : Semiring R
a✝ b✝ : α
e : Sym2 α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : ¬a = b
h' : ¬Adj G a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0
[PROOFSTEP]
simp only [Matrix.mul_apply, Matrix.transpose_apply, G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h',
  sum_const_zero]


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ 0 ≤ energy P G
[PROOFSTEP]
refine' div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| sq_nonneg _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card (offDiag P.parts)) ≤ 1 * ↑(card P.parts) ^ 2
[PROOFSTEP]
rw [offDiag_card, one_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card P.parts * card P.parts - card P.parts) ≤ ↑(card P.parts) ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts * card P.parts
[PROOFSTEP]
exact tsub_le_self
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑(energy P G) = (∑ uv in offDiag P.parts, ↑(SimpleGraph.edgeDensity G uv.fst uv.snd) ^ 2) / ↑(card P.parts) ^ 2
[PROOFSTEP]
rw [energy]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑((∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(card P.parts) ^ 2) =
    (∑ uv in offDiag P.parts, ↑(SimpleGraph.edgeDensity G uv.fst uv.snd) ^ 2) / ↑(card P.parts) ^ 2
[PROOFSTEP]
norm_cast