Theorem: SimpleGraph.copyCount_le_labelledCopyCount (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✝ : Fintype β
⊢ G.copyCount H ≤ G.labelledCopyCount H
Tactic:
rw [copyCount, ← Fintype.card_coe]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype.card { x // x ∈ filter (fun H' => Nonempty (G ≃g H'.coe)) univ } ≤ G.labelledCopyCount H

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype.card { x // x ∈ filter (fun H' => Nonempty (G ≃g H'.coe)) univ } ≤ G.labelledCopyCount H
Tactic:
refine Fintype.card_le_of_injective (fun H' ↦
  ⟨H'.val.hom.comp (mem_filter.1 H'.2).2.some.toHom,
    Subtype.coe_injective.comp (mem_filter.1 H'.2).2.some.injective⟩) ?_
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Injective fun H' => ⟨(↑H').hom.comp ⋯.some.toHom, ⋯⟩

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Injective fun H' => ⟨(↑H').hom.comp ⋯.some.toHom, ⋯⟩
Tactic:
sorry
State after:
no goals