Theorem: SimpleGraph.isContained_iff_exists_subgraph (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 γ
⊢ G ⊑ H ↔ ∃ H', Nonempty (G ≃g H'.coe)
Tactic:
constructor
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

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⟩
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)

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⟩⟩
State after:
no goals

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⟩⟩
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

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
State after:
no goals