internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.facets_mono
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
⊢ K₁.facets ⊆ K₂.facets
Tactic:
refine' fun s hs => ⟨h hs.1, fun t ht hst => Finset.eq_of_subset_of_card_le hst _⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ s.card
Theorem: Geometry.SimplicialComplex.facets_mono
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ s.card
Tactic:
rw [hK₁.2 hs]
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ n + 1
Theorem: Geometry.SimplicialComplex.facets_mono
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ n + 1
Tactic:
exact hK₂.card_le ht
Proof state after:
no goals
Theorem: SimpleGraph.isContained_iff_exists_subgraph
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊑ H ↔ ∃ H', Nonempty (G ≃g H'.coe)
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊑ H → ∃ H', Nonempty (G ≃g H'.coe)

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (∃ H', Nonempty (G ≃g H'.coe)) → G ⊑ H
Theorem: SimpleGraph.isContained_iff_exists_subgraph
Proof state before:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊑ H → ∃ H', Nonempty (G ≃g H'.coe)
Tactic:
rintro ⟨f, hf⟩
Proof state after:
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G →g H
hf : Injective ⇑f
⊢ ∃ H', Nonempty (G ≃g H'.coe)
Theorem: SimpleGraph.isContained_iff_exists_subgraph
Proof state before:
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G →g H
hf : Injective ⇑f
⊢ ∃ H', Nonempty (G ≃g H'.coe)
Tactic:
exact ⟨Subgraph.map f ⊤, ⟨(Subgraph.isoMap _ hf _).comp Subgraph.topIso.symm⟩⟩
Proof state after:
no goals
Theorem: SimpleGraph.isContained_iff_exists_subgraph
Proof state before:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (∃ H', Nonempty (G ≃g H'.coe)) → G ⊑ H
Tactic:
rintro ⟨H', ⟨e⟩⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
H' : H.Subgraph
e : G ≃g H'.coe
⊢ G ⊑ H
Theorem: SimpleGraph.isContained_iff_exists_subgraph
Proof state before:
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
H' : H.Subgraph
e : G ≃g H'.coe
⊢ G ⊑ H
Tactic:
exact e.isContained.trans H'.coe_isContained
Proof state after:
no goals
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊴ H ↔ ∃ H' _e, H'.IsInduced'
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊴ H → ∃ H' _e, H'.IsInduced'

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (∃ H' _e, H'.IsInduced') → G ⊴ H
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊴ H → ∃ H' _e, H'.IsInduced'
Tactic:
rintro ⟨f⟩
Proof state after:
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
⊢ ∃ H' _e, H'.IsInduced'
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
⊢ ∃ H' _e, H'.IsInduced'
Tactic:
refine' ⟨Subgraph.map f.toHom ⊤,
  (Subgraph.isoMap f.toHom f.injective _).comp Subgraph.topIso.symm, _⟩
Proof state after:
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
⊢ (Subgraph.map f.toHom ⊤).IsInduced'
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
⊢ (Subgraph.map f.toHom ⊤).IsInduced'
Tactic:
rintro _ _ ⟨a, -, rfl⟩ ⟨b, -, rfl⟩
Proof state after:
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
a b : α
⊢ H.Adj (f.toHom a) (f.toHom b) → (Subgraph.map f.toHom ⊤).Adj (f.toHom a) (f.toHom b)
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
a b : α
⊢ H.Adj (f.toHom a) (f.toHom b) → (Subgraph.map f.toHom ⊤).Adj (f.toHom a) (f.toHom b)
Tactic:
simp [Relation.map_apply_apply, f.injective]
Proof state after:
no goals
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (∃ H' _e, H'.IsInduced') → G ⊴ H
Tactic:
rintro ⟨H', e, hH'⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
H' : H.Subgraph
e : G ≃g H'.coe
hH' : H'.IsInduced'
⊢ G ⊴ H
Theorem: SimpleGraph.isIndContained_iff_exists_subgraph
Proof state before:
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
H' : H.Subgraph
e : G ≃g H'.coe
hH' : H'.IsInduced'
⊢ G ⊴ H
Tactic:
exact e.isIndContained.trans hH'.isIndContained
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_bot
Proof 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]
Proof 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
Theorem: SimpleGraph.copyCount_bot
Proof 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)
Proof 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 := ⋯ }}
Theorem: SimpleGraph.copyCount_bot
Proof 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]
Proof 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 := ⋯ }
Theorem: SimpleGraph.copyCount_bot
Proof 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) _⟩
Proof 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
Theorem: SimpleGraph.copyCount_bot
Proof 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
Proof 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
Theorem: SimpleGraph.copyCount_bot
Proof 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]
Proof 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
Theorem: SimpleGraph.copyCount_bot
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_bot
Proof 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]
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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]
Proof 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
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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)
Proof 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 = {⊥}
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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 ⊥]
Proof 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 = ⊥
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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
Proof 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 = ⊥
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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 ↦ _⟩
Proof 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
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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]
Proof 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
Theorem: SimpleGraph.copyCount_of_isEmpty
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_eq_zero
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
⊢ G.copyCount H = 0 ↔ ¬G ⊑ H
Tactic:
simp [copyCount, isContained_iff_exists_subgraph, card_pos, filter_eq_empty_iff]
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_pos
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
⊢ 0 < G.copyCount H ↔ G ⊑ H
Tactic:
simp [copyCount, isContained_iff_exists_subgraph, card_pos, filter_nonempty_iff]
Proof state after:
no goals
Theorem: SimpleGraph.labelledCopyCount_of_isEmpty
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ G.labelledCopyCount H = 1
Tactic:
convert Fintype.card_unique
Proof state after:
case convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ Unique { f // Injective ⇑f }
Theorem: SimpleGraph.labelledCopyCount_of_isEmpty
Proof state before:
case convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ Unique { f // Injective ⇑f }
Tactic:
exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
Proof state after:
no goals
Theorem: SimpleGraph.labelledCopyCount_eq_zero
Proof 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.labelledCopyCount H = 0 ↔ ¬G ⊑ H
Tactic:
simp [labelledCopyCount, IsContained, Fintype.card_eq_zero_iff]
Proof state after:
no goals
Theorem: SimpleGraph.labelledCopyCount_pos
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 0 < G.labelledCopyCount H ↔ G ⊑ H
Tactic:
simp [labelledCopyCount, IsContained, Fintype.card_pos_iff]
Proof state after:
no goals
Theorem: SimpleGraph.copyCount_le_labelledCopyCount
Proof 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]
Proof 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
Theorem: SimpleGraph.copyCount_le_labelledCopyCount
Proof 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⟩) ?_
Proof 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, ⋯⟩
Theorem: SimpleGraph.copyCount_le_labelledCopyCount
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.aux
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : H.Subgraph
⊢ Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty
Tactic:
obtain ⟨e, he⟩ := edgeSet_nonempty.2 hG
Proof state after:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : H.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty
Theorem: SimpleGraph.aux
Proof state before:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : H.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty
Tactic:
rw [← Subgraph.image_coe_edgeSet_coe]
Proof state after:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : H.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → (Sym2.map Subtype.val '' H'.coe.edgeSet).Nonempty
Theorem: SimpleGraph.aux
Proof state before:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : H.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → (Sym2.map Subtype.val '' H'.coe.edgeSet).Nonempty
Tactic:
exact fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩
Proof state after:
no goals
Theorem: SimpleGraph.kill_le
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G.kill H ≤ H
Tactic:
rw [kill]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (if hG : G = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})) ≤ H
Theorem: SimpleGraph.kill_le
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ (if hG : G = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})) ≤ H
Tactic:
split_ifs
Proof state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
h✝ : G = ⊥
⊢ H ≤ H

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
h✝ : ¬G = ⊥
⊢ H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some}) ≤ H