awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ ¬?_mvar.34363

Tactic:
f.map_mem_edgeSet h.choose_spec

Premises used: Exists.choose_spec, SimpleGraph.Hom.map_mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
absurd : Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ edgeSet ⊥
⊢ False

Tactic:
absurd f.map_mem_edgeSet h.choose_spec

Premises used: Exists.choose_spec, SimpleGraph.Hom.map_mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
rw : Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ ∅
⊢ Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ edgeSet ⊥

Tactic:
rw [edgeSet_bot]

Premises used: SimpleGraph.edgeSet_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ ∅

Tactic:
Set.notMem_empty (h.choose.map f)

Premises used: Sym2.map, Set.notMem_empty, Exists.choose, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : Hom.{u_4, u_5} (W := β) A ⊥
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Sym2.map (⇑f : (a : α) → β) (Exists.choose (p := Membership.mem A.edgeSet) h) ∉ ∅

Tactic:
exact Set.notMem_empty (h.choose.map f)

Premises used: Sym2.map, Set.notMem_empty, Exists.choose, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G.Copy H
⊢ G ⊑ H

Tactic:
⟨f⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ G ⊴ H

Tactic:
⟨f⟩

Premises used: SimpleGraph.IsIndContained, Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ G ⊑ H

Tactic:
f.toCopy.isContained

Premises used: SimpleGraph.Copy.isContained, SimpleGraph.Embedding.toCopy
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G ⊴ H → G ⊑ H

Tactic:
fun ⟨f⟩ ↦ f.isContained

Premises used: SimpleGraph.IsContained, _private.0.SimpleGraph.IsIndContained.isContained.match_1, SimpleGraph.Embedding.isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ G ⊑ H

Tactic:
e.toCopy.isContained

Premises used: SimpleGraph.Iso.toCopy, SimpleGraph.Copy.isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ H ⊑ G

Tactic:
e.symm.isContained

Premises used: SimpleGraph.Iso.isContained, SimpleGraph.Iso.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ G ⊴ H

Tactic:
e.toEmbedding.isIndContained

Premises used: SimpleGraph.Iso.toEmbedding, SimpleGraph.Embedding.isIndContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ H ⊴ G

Tactic:
e.symm.isIndContained

Premises used: SimpleGraph.Iso.symm, SimpleGraph.Iso.isIndContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
hG' : G'.IsInduced
⊢ G'.coe ⊴ G

Tactic:
⟨{ toFun := (↑)
     inj' := Subtype.coe_injective
     map_rel_iff' := hG'.adj.symm }⟩

Premises used: RelEmbedding.mk, SimpleGraph.Subgraph.IsInduced.adj, Function.Embedding.mk, SimpleGraph.IsIndContained, Nonempty.intro, Subtype.coe_injective, Subtype.val, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G ⊴ G

Tactic:
⟨Embedding.refl⟩

Premises used: SimpleGraph.IsIndContained, Nonempty.intro, SimpleGraph.Embedding.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G ⊴ G

Tactic:
.refl _

Premises used: SimpleGraph.IsIndContained.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
⊢ G ⊴ H → H ⊴ I → G ⊴ I

Tactic:
fun ⟨f⟩ ⟨g⟩ ↦ ⟨g.comp f⟩

Premises used: _private.0.SimpleGraph.IsIndContained.isContained.match_1, SimpleGraph.IsIndContained, Nonempty.intro, SimpleGraph.Embedding.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : IsEmpty V
⊢ G ⊴ H

Tactic:
⟨{ toFun := isEmptyElim
     inj' := isEmptyElim
     map_rel_iff' := fun {a} ↦ isEmptyElim a }⟩

Premises used: RelEmbedding.mk, isEmptyElim, Function.Embedding.mk, SimpleGraph.IsIndContained, Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
mp : G ⊴ H → ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced
mpr : (∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced) → G ⊴ H
⊢ G ⊴ H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced

Tactic:
⟨Subgraph.map f.toHom ⊤, f.toCopy.isoToSubgraph, ?_⟩

Premises used: SimpleGraph.Subgraph.map, Exists.intro, Top.top, SimpleGraph.Copy.isoToSubgraph, SimpleGraph.Embedding.toHom, SimpleGraph.Embedding.toCopy
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
mp : (Subgraph.map f.toHom ⊤).IsInduced
⊢ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced

Tactic:
refine ⟨Subgraph.map f.toHom ⊤, f.toCopy.isoToSubgraph, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ (Subgraph.map f.toHom ⊤).IsInduced

Tactic:
simp [Subgraph.IsInduced, Relation.map_apply_apply, f.injective]

Premises used: RelEmbedding.injective, Relation.map_apply_apply, SimpleGraph.Subgraph.IsInduced
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
H' : H.Subgraph
e : G ≃g H'.coe
hH' : H'.IsInduced
⊢ G ⊴ H

Tactic:
e.isIndContained.trans hH'.isIndContained

Premises used: SimpleGraph.IsIndContained.trans, SimpleGraph.Iso.isIndContained, SimpleGraph.Subgraph.IsInduced.isIndContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
H' : H.Subgraph
e : G ≃g H'.coe
hH' : H'.IsInduced
⊢ G ⊴ H

Tactic:
exact e.isIndContained.trans hH'.isIndContained

Premises used: SimpleGraph.IsIndContained.trans, SimpleGraph.Iso.isIndContained, SimpleGraph.Subgraph.IsInduced.isIndContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G ⊴ H ↔ ∃ (s : Set W), Nonempty (G ≃g induce s H)

Tactic:
⟨fun ⟨f⟩ ↦ ⟨Set.range f, ⟨f.isoInduceRange⟩⟩, fun ⟨s, ⟨f⟩⟩ ↦ ⟨.comp (.induce s) f⟩⟩

Premises used: SimpleGraph.Iso, _private.0.SimpleGraph.isIndContained_iff_exists_iso_induce.match_1, _private.0.SimpleGraph.IsIndContained.isContained.match_1, Exists, SimpleGraph.Embedding.isoInduceRange, SimpleGraph.IsIndContained, Nonempty.intro, Iff.intro, Exists.intro, Nonempty, SimpleGraph.induce, RelIso.toRelEmbedding, Set.range, DFunLike.coe, SimpleGraph.Embedding.induce, SimpleGraph.Embedding.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
H : SimpleGraph W
⊢ IsIndContained.{u_1, u_2} (V := V) ⊤ H ↔ IsContained.{u_1, u_2} (α := V) ⊤ H

Tactic:
⟨IsIndContained.isContained, fun ⟨f⟩ ↦ ⟨f.topEmbedding⟩⟩

Premises used: _private.0.SimpleGraph.top_isIndContained_iff_top_isContained.match_1, SimpleGraph.Copy.topEmbedding, SimpleGraph.IsIndContained, SimpleGraph.IsIndContained.isContained, Nonempty.intro, Iff.intro, Top.top
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ Gᶜ ⊴ Hᶜ ↔ G ⊴ H

Tactic:
Embedding.complEquiv.symm.nonempty_congr

Premises used: SimpleGraph.IsIndContained, Equiv.nonempty_congr, Equiv.symm, SimpleGraph.Embedding.complEquiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ H ⊑ G ↔ ∃ (f : W ↪ V), H ≤ SimpleGraph.comap (⇑f : (a : W) → V) G

Tactic:
⟨fun ⟨f⟩ ↦ ⟨f.toEmbedding, f.toHom.le_comap⟩, fun ⟨f, h⟩ ↦ ⟨⟨f, (h ·)⟩, f.injective⟩⟩

Premises used: SimpleGraph.Copy.mk, SimpleGraph.IsContained, Exists, LE.le, SimpleGraph.Hom.le_comap, Nonempty.intro, _private.0.SimpleGraph.isContained_iff_exists_le_comap.match_2, SimpleGraph.Copy.toEmbedding, SimpleGraph.comap, _private.0.SimpleGraph.isContained_iff_exists_le_comap.match_1, Iff.intro, Exists.intro, Function.Embedding.injective, SimpleGraph.Copy.toHom, RelHom.mk, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ H ⊴ G ↔ ∃ (f : W ↪ V), SimpleGraph.comap (⇑f : (a : W) → V) G = H

Tactic:
⟨fun ⟨f⟩ ↦ ⟨f.toEmbedding, f.comap_eq⟩, fun ⟨f, h⟩ ↦ ⟨f, h ▸ .rfl⟩⟩

Premises used: RelEmbedding.mk, _private.0.SimpleGraph.isIndContained_iff_exists_comap_eq.match_2, SimpleGraph.Embedding.comap_eq, Iff.rfl, _private.0.SimpleGraph.isIndContained_iff_exists_comap_eq.match_1, Exists, Eq.rec, SimpleGraph.IsIndContained, RelEmbedding.toEmbedding, Nonempty.intro, SimpleGraph.comap, Iff.intro, Exists.intro, Eq, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G_1 G₁ G₂ G₃ : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst : Fintype V
inst_1 : Fintype W
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
exact Fintype.card (Copy H G)

Premises used: SimpleGraph.Copy, Fintype.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G_1 G₁ G₂ G₃ : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst : Fintype V
inst_1 : Fintype W
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
classical exact Fintype.card (Copy H G)
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : Fintype W
inst_2 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ Fintype.card (H.Copy G) = 1

Tactic:
Fintype.card_unique

Premises used: Fintype.card_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : Fintype W
inst_2 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
convert_2 : Unique (H.Copy G)
⊢ G.labelledCopyCount H = 1

Tactic:
convert! Fintype.card_unique

Premises used: Fintype.card_unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : Fintype W
inst_2 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ Unique (H.Copy G)

Tactic:
exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
⊢ G.labelledCopyCount H = 0 ↔ H.Free G

Tactic:
simp [labelledCopyCount, Fintype.card_eq_zero_iff]

Premises used: SimpleGraph.labelledCopyCount, Fintype.card_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
⊢ 0 < G.labelledCopyCount H ↔ H ⊑ G

Tactic:
simp [labelledCopyCount, IsContained, Fintype.card_pos_iff]

Premises used: SimpleGraph.IsContained, SimpleGraph.labelledCopyCount, Fintype.card_pos_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G_1 G₁ G₂ G₃ : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst : Fintype V
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}

Premises used: SimpleGraph.Subgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G_1 G₁ G₂ G₃ : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst : Fintype V
G : SimpleGraph V
H : SimpleGraph W
⊢ ℕ

Tactic:
classical exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}

Premises used: SimpleGraph.Subgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype { f : H →g G // Injective.{u_2 + 1, u_1 + 1} (α := W) (β := V) (⇑f : (a : W) → V) }
inst_2 : DecidableEq G.Subgraph
e_s :
  Eq.{u_1 + 1} (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
    (image (α := H.Copy G) Copy.toSubgraph univ)
⊢ Finset.card.{u_1} (α := G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)} =
    Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ)

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype { f : H →g G // Injective.{u_2 + 1, u_1 + 1} (α := W) (β := V) (⇑f : (a : W) → V) }
inst_2 : DecidableEq G.Subgraph
⊢ Eq.{u_1 + 1} (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
    (image (α := H.Copy G) Copy.toSubgraph univ)

Tactic:
Finset.coe_injective ?_

Premises used: Finset.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype { f : H →g G // Injective.{u_2 + 1, u_1 + 1} (α := W) (β := V) (⇑f : (a : W) → V) }
inst_2 : DecidableEq G.Subgraph
e_s :
  (↑{G' : G.Subgraph | Nonempty (H ≃g G'.coe)} : Set G.Subgraph) =
    (↑(image (α := H.Copy G) Copy.toSubgraph univ) : Set G.Subgraph)
⊢ Eq.{u_1 + 1} (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
    (image (α := H.Copy G) Copy.toSubgraph univ)

Tactic:
refine Finset.coe_injective ?_

Premises used: Finset.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype { f : H →g G // Injective.{u_2 + 1, u_1 + 1} (α := W) (β := V) (⇑f : (a : W) → V) }
inst_2 : DecidableEq G.Subgraph
⊢ (↑{G' : G.Subgraph | Nonempty (H ≃g G'.coe)} : Set G.Subgraph) =
    (↑(image (α := H.Copy G) Copy.toSubgraph univ) : Set G.Subgraph)

Tactic:
simpa [-Copy.range_toSubgraph] using Copy.range_toSubgraph.symm

Premises used: SimpleGraph.Copy.range_toSubgraph, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
⊢ G.copyCount H = 0 ↔ H.Free G

Tactic:
simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
    filter_eq_empty_iff]

Premises used: SimpleGraph.Free, SimpleGraph.isContained_iff_exists_iso_subgraph, SimpleGraph.copyCount, Finset.filter_eq_empty_iff, nonempty_subtype
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
⊢ 0 < G.copyCount H ↔ H ⊑ G

Tactic:
simp [copyCount, -nonempty_subtype, isContained_iff_exists_iso_subgraph, card_pos,
    filter_nonempty_iff]

Premises used: SimpleGraph.isContained_iff_exists_iso_subgraph, Finset.filter_nonempty_iff, SimpleGraph.copyCount, nonempty_subtype, Finset.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
rw : Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ) ≤ G.labelledCopyCount H
⊢ G.copyCount H ≤ G.labelledCopyCount H

Tactic:
rw [copyCount_eq_card_image_copyToSubgraph]

Premises used: SimpleGraph.copyCount_eq_card_image_copyToSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
⊢ Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ) ≤ G.labelledCopyCount H

Tactic:
card_image_le

Premises used: SimpleGraph.labelledCopyCount, Fintype.card, Finset.card_image_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
⊢ Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ) ≤ G.labelledCopyCount H

Tactic:
exact card_image_le

Premises used: Finset.card_image_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
classical classical₁ classical₂ classical₃ :
  Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ) ≤ G.labelledCopyCount H
⊢ G.copyCount H ≤ G.labelledCopyCount H

Tactic:
classical rw [copyCount_eq_card_image_copyToSubgraph]; exact card_image_le

Premises used: Finset.card_image_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
⊢ Finset.card (α := G.Subgraph)
      {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ : G.Subgraph }} =
    1

Tactic:
card_singleton (α := G.Subgraph)
      { verts := .univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim }

Premises used: SimpleGraph.Subgraph.mk, Set.univ, False.elim, Bot.bot, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
h :
  Eq (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)}
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}
⊢ Finset.card.{u_1} (α := G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)} = 1

Tactic:
convert!
    card_singleton (α := G.Subgraph)
      { verts := .univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim }

Premises used: SimpleGraph.Subgraph.mk, Set.univ, False.elim, Bot.bot, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
h :
  Nonempty.{u_1 + 1}
      (Iso (V := V) (W := (↑Set.univ : Type u_1)) ⊥
        (Subgraph.coe { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } :
          SimpleGraph
            (↑(Subgraph.verts (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) :
              Type u_1))) ∧
    ∀ (x : G.Subgraph) (a : Iso (V := V) ⊥ x.coe),
      x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
⊢ Eq (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)}
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}

Tactic:
simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]

Premises used: Nonempty.forall, Finset.mem_filter_univ, Finset.eq_singleton_iff_unique_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
⊢ ∀ {a b : V},
    Adj.{u_1} (V := (↑Set.univ : Type u_1))
        (Subgraph.coe { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } :
          SimpleGraph
            (↑(Subgraph.verts (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) :
              Type u_1))
        (((Equiv.Set.univ V).symm : (a : V) → (↑Set.univ : Type u_1)) a)
        (((Equiv.Set.univ V).symm : (a : V) → (↑Set.univ : Type u_1)) b) ↔
      Adj ⊥ a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
h :
  ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe),
    H'.Adj = Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
⊢ Nonempty.{u_1 + 1}
      (Iso (V := V) (W := (↑Set.univ : Type u_1)) ⊥
        (Subgraph.coe { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } :
          SimpleGraph
            (↑(Subgraph.verts (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) :
              Type u_1))) ∧
    ∀ (x : G.Subgraph) (a : Iso (V := V) ⊥ x.coe),
      x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

Tactic:
refine ⟨⟨⟨(Equiv.Set.univ _).symm, by simp⟩⟩, fun H' e ↦
    Subgraph.ext ((set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm) ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
H' : G.Subgraph
e : Iso (V := V) ⊥ H'.coe
h :
  ∀ (a b : V),
    H'.Adj a b ↔ Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } a b
⊢ H'.Adj = Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

Tactic:
ext a b
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
H' : G.Subgraph
e : Iso (V := V) ⊥ H'.coe
a b : V
h : ¬H'.Adj a b
⊢ H'.Adj a b ↔ Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } a b

Tactic:
simp only [Prop.bot_eq_false, Pi.bot_apply, iff_false]

Premises used: iff_false, Prop.bot_eq_false, Pi.bot_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
H' : G.Subgraph
e : Iso (V := V) ⊥ H'.coe
a b : V
⊢ ¬H'.Adj a b

Tactic:
fun hab ↦ e.symm.map_rel_iff.2 hab.coe

Premises used: Iff.mpr, RelIso.map_rel_iff, SimpleGraph.Iso.symm, SimpleGraph.Subgraph.Adj.coe, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
H' : G.Subgraph
e : Iso (V := V) ⊥ H'.coe
a b : V
⊢ ¬H'.Adj a b

Tactic:
exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe

Premises used: Iff.mpr, RelIso.map_rel_iff, SimpleGraph.Iso.symm