rintro ⟨f⟩
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 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'