Theorem: SimpleGraph.copyCount_bot (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 β
H : SimpleGraph β
⊢ ⊥.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 β
H : SimpleGraph β
⊢ (filter (fun H' => Nonempty (⊥ ≃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 β
H : SimpleGraph β
⊢ (filter (fun H' => Nonempty (⊥ ≃g H'.coe)) univ).card = 1
Tactic:
convert
  card_singleton
    ({  verts := Set.univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim } : 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 β
H : SimpleGraph β
⊢ filter (fun H' => Nonempty (⊥ ≃g H'.coe)) univ =
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}

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 β
H : SimpleGraph β
⊢ filter (fun H' => Nonempty (⊥ ≃g H'.coe)) univ =
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}
Tactic:
simp only [eq_singleton_iff_unique_mem, mem_filter, mem_univ, Subgraph.coe_bot, true_and_iff,
  Nonempty.forall]
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 β
H : SimpleGraph β
⊢ Nonempty (⊥ ≃g { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe) ∧
    ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

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 β
H : SimpleGraph β
⊢ Nonempty (⊥ ≃g { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe) ∧
    ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
Tactic:
refine'
  ⟨⟨⟨(Equiv.Set.univ _).symm, by
    simp only [Prop.bot_eq_false, Subgraph.coe_adj, Pi.bot_apply, bot_adj, iff_self_iff,
      forall₂_true_iff]⟩⟩, fun H' e ↦
    Subgraph.ext _ _ ((set_fintype_card_eq_univ_iff _).1 $ Fintype.card_congr e.toEquiv.symm) _⟩
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 β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.Adj = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj

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 β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.Adj = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj
Tactic:
ext a b
State after:
case h.e'_2.h.e'_2.h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ H'.Adj a b ↔ { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj a b

State before:
case h.e'_2.h.e'_2.h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ H'.Adj a b ↔ { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj a b
Tactic:
simp only [Prop.bot_eq_false, Pi.bot_apply, iff_false_iff]
State after:
case h.e'_2.h.e'_2.h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ ¬H'.Adj a b

State before:
case h.e'_2.h.e'_2.h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
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

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
⊢ ∀ {a b : β},
    { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe.Adj ((Equiv.Set.univ β).symm a)
        ((Equiv.Set.univ β).symm b) ↔
      ⊥.Adj a b
Tactic:
simp only [Prop.bot_eq_false, Subgraph.coe_adj, Pi.bot_apply, bot_adj, iff_self_iff,
  forall₂_true_iff]
State after:
no goals