Theorem: SimpleGraph.copyCount_of_isEmpty (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ G.copyCount H = 1
Tactic:
rw [copyCount]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ (filter (fun H' => Nonempty (G ≃g H'.coe)) univ).card = 1

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ (filter (fun H' => Nonempty (G ≃g H'.coe)) univ).card = 1
Tactic:
convert card_singleton (⊥ : H.Subgraph)
State after:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ filter (fun H' => Nonempty (G ≃g H'.coe)) univ = {⊥}

State before:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ filter (fun H' => Nonempty (G ≃g H'.coe)) univ = {⊥}
Tactic:
simp only [eq_singleton_iff_unique_mem, mem_filter, mem_univ, Subgraph.coe_bot, true_and_iff,
  Nonempty.forall, Subsingleton.elim G ⊥]
State after:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥

State before:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥
Tactic:
haveI : IsEmpty (⊥ : H.Subgraph).verts := by simp
State after:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥

State before:
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥
Tactic:
refine' ⟨⟨⟨⟨isEmptyElim, isEmptyElim, isEmptyElim, isEmptyElim⟩, fun {a} ↦ isEmptyElim a⟩⟩,
  fun H' e ↦ Subgraph.ext _ _ _ $ funext₂ fun a b ↦ _⟩
State after:
case h.e'_2.h.e'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.verts = ⊥.verts

case h.e'_2.h.e'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ H'.Adj a b = ⊥.Adj a b

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ IsEmpty ↑⊥.verts
Tactic:
simp
State after:
no goals

State before:
case h.e'_2.h.e'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.verts = ⊥.verts
Tactic:
simpa [Set.eq_empty_iff_forall_not_mem, filter_eq_empty_iff, ‹IsEmpty α›] using
  e.toEquiv.symm.isEmpty_congr
State after:
no goals

State before:
case h.e'_2.h.e'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ H'.Adj a b = ⊥.Adj a b
Tactic:
simp only [Subgraph.not_bot_adj, eq_iff_iff, iff_false_iff]
State after:
case h.e'_2.h.e'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ ¬H'.Adj a b

State before:
case h.e'_2.h.e'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ ¬H'.Adj a b
Tactic:
exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe
State after:
no goals