Theorem: SimpleGraph.isIndContained_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' _e, H'.IsInduced'
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' _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

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

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, _⟩
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'

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

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]
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' _e, H'.IsInduced') → G ⊴ H
Tactic:
rintro ⟨H', e, hH'⟩
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

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