internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.kill_le
Proof state before:
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
Tactic:
exacts [le_rfl, deleteEdges_le _]
Proof state after:
no goals
Theorem: SimpleGraph.bot_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
H : SimpleGraph β
⊢ ⊥.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 γ
H : SimpleGraph β
⊢ (if hG : ⊥ = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (⊥ ≃g H'.coe)), {⋯.some})) = H
Theorem: SimpleGraph.bot_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
H : SimpleGraph β
⊢ (if hG : ⊥ = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (⊥ ≃g H'.coe)), {⋯.some})) = H
Tactic:
exact dif_pos rfl
Proof state after:
no goals
Theorem: SimpleGraph.kill_of_ne_bot
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H : SimpleGraph β
⊢ G.kill H = H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Tactic:
rw [kill]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H : SimpleGraph β
⊢ (if hG : G = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})) =
    H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Theorem: SimpleGraph.kill_of_ne_bot
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H : SimpleGraph β
⊢ (if hG : G = ⊥ then H else H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})) =
    H.deleteEdges (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Tactic:
exact dif_neg hG
Proof state after:
no goals
Theorem: SimpleGraph.kill_eq_right
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ G.kill H = H ↔ ¬G ⊑ H
Tactic:
simp only [kill_of_ne_bot hG, Set.disjoint_left, isContained_iff_exists_subgraph,
  @forall_swap _ H.Subgraph, Set.iUnion_singleton_eq_range, deleteEdges_eq_self, Set.mem_iUnion,
  Set.mem_range, not_exists, not_nonempty_iff, Nonempty.forall]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ (∀ (y : H.Subgraph), ∀ x ∈ H.edgeSet, ∀ (a : G ≃g y.coe), x ∉ {⋯.some}) ↔ ∀ (x : H.Subgraph), IsEmpty (G ≃g x.coe)
Theorem: SimpleGraph.kill_eq_right
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ (∀ (y : H.Subgraph), ∀ x ∈ H.edgeSet, ∀ (a : G ≃g y.coe), x ∉ {⋯.some}) ↔ ∀ (x : H.Subgraph), IsEmpty (G ≃g x.coe)
Tactic:
exact forall_congr' fun H' ↦ ⟨fun h ↦ ⟨fun f ↦ h _
  (Subgraph.edgeSet_subset _ $ (aux hG ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩
Proof state after:
no goals
Theorem: SimpleGraph.kill_of_not_isContained
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
⊢ G.kill H = H
Tactic:
obtain rfl | hG := eq_or_ne G ⊥
Proof state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬⊥ ⊑ H
⊢ ⊥.kill H = H

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
hG : G ≠ ⊥
⊢ G.kill H = H
Theorem: SimpleGraph.kill_of_not_isContained
Proof state before:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬⊥ ⊑ H
⊢ ⊥.kill H = H
Tactic:
exact bot_kill _
Proof state after:
no goals
Theorem: SimpleGraph.kill_of_not_isContained
Proof state before:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
hG : G ≠ ⊥
⊢ G.kill H = H
Tactic:
exact (kill_eq_right hG).2 hGH
Proof state after:
no goals
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬G ⊑ G.kill H
Tactic:
rw [kill_of_ne_bot hG, deleteEdges, isContained_iff_exists_subgraph]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬∃ H', Nonempty (G ≃g H'.coe)
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬∃ H', Nonempty (G ≃g H'.coe)
Tactic:
rintro ⟨H', hGH'⟩
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
⊢ False
Tactic:
have hH' : (H'.map $ Hom.ofLE (sdiff_le : H \ _ ≤ H)).edgeSet.Nonempty := by
  rw [Subgraph.edgeSet_map]
  exact (aux hG hGH').image _
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
⊢ False
Tactic:
set e := hH'.some with he
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β := hH'.some
he : e = hH'.some
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β := hH'.some
he : e = hH'.some
⊢ False
Tactic:
have : e ∈ _ := hH'.some_mem
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β := hH'.some
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β := hH'.some
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False
Tactic:
clear_value e
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False
Tactic:
rw [← Subgraph.image_coe_edgeSet_coe] at this
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β
he : e = hH'.some
this : e ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 β
he : e = hH'.some
this : e ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False
Tactic:
subst he
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
this : hH'.some ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
this : hH'.some ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False
Tactic:
obtain ⟨e, he₀, he₁⟩ := this
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
⊢ False
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
⊢ False
Tactic:
let e' : Sym2 H'.verts := Sym2.map (Subgraph.isoMap (Hom.ofLE _) injective_id _).symm e
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
⊢ False
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
⊢ False
Tactic:
have he' : e' ∈ H'.coe.edgeSet := (Iso.map_mem_edgeSet_iff _).2 he₀
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ H'.coe.edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ H'.coe.edgeSet
⊢ False
Tactic:
rw [Subgraph.edgeSet_coe] at he'
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
⊢ False
Tactic:
have := Subgraph.edgeSet_subset _ he'
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this : Sym2.map Subtype.val e' ∈ (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).edgeSet
⊢ False
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this : Sym2.map Subtype.val e' ∈ (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).edgeSet
⊢ False
Tactic:
simp only [edgeSet_sdiff,  edgeSet_fromEdgeSet,  edgeSet_sdiff_sdiff_isDiag, Set.mem_diff,
  Set.mem_iUnion, not_exists] at this
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ False
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ False
Tactic:
refine' this.2 (H'.map $ Hom.ofLE sdiff_le)
  ⟨(Subgraph.isoMap (Hom.ofLE _) injective_id _).comp hGH'.some⟩ _
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map Subtype.val e' ∈ {⋯.some}
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map Subtype.val e' ∈ {⋯.some}
Tactic:
rw [Sym2.map_map, Set.mem_singleton_iff, ← he₁]
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e = Sym2.map Subtype.val e
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e = Sym2.map Subtype.val e
Tactic:
congr 1 with x
Proof state after:
case intro.intro.intro.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
x : ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
⊢ (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) x = ↑x
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
case intro.intro.intro.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
x : ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
⊢ (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) x = ↑x
Tactic:
refine' congr_arg (↑) (Equiv.Set.image_symm_apply _ _ injective_id _ _)
Proof state after:
no goals