-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem map_edgeFinset_induce :
    (G.induce s).edgeFinset.map (Embedding.subtype s).sym2Map
      = G.edgeFinset ∩ s.toFinset.sym2

Proof state:
case mp.intro.intro.intro.inr.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hw : ↑x = w
hv : ↑y = v
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s

Tactic:
rw [← hv, ← hw]

Result:
case mp.intro.intro.intro.inr.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hw : ↑x = w
hv : ↑y = v
⊢ G.Adj ↑y ↑x ∧ ↑y ∈ s ∧ ↑x ∈ s

Proof state:
case mp.intro.intro.intro.inl.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hv : ↑x = v
hw : ↑y = w
⊢ G.Adj ↑x ↑y ∧ ↑x ∈ s ∧ ↑y ∈ s

Tactic:
exact ⟨hadj, x.prop, y.prop⟩

Result:
no goals

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ map (Embedding.subtype s).sym2Map (induce s G).edgeFinset = G.edgeFinset ∩ s.toFinset.sym2

Tactic:
simp_rw [Finset.ext_iff, Sym2.forall, mem_inter, mk_mem_sym2_iff, mem_map, Sym2.exists,
  Set.mem_toFinset, mem_edgeSet, comap_adj, Embedding.sym2Map_apply, Embedding.coe_subtype,
  Sym2.map_pair_eq, Sym2.eq_iff]

Result:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ ∀ (x y : V), (∃ x_1 y_1, G.Adj ↑x_1 ↑y_1 ∧ (↑x_1 = x ∧ ↑y_1 = y ∨ ↑x_1 = y ∧ ↑y_1 = x)) ↔ G.Adj x y ∧ x ∈ s ∧ y ∈ s

Proof state:
case mp.intro.intro.intro.inl.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hv : ↑x = v
hw : ↑y = w
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s

case mp.intro.intro.intro.inr.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hw : ↑x = w
hv : ↑y = v
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s

Tactic:
all_goals rw [← hv, ← hw]

Result:
case mp.intro.intro.intro.inl.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hv : ↑x = v
hw : ↑y = w
⊢ G.Adj ↑x ↑y ∧ ↑x ∈ s ∧ ↑y ∈ s

case mp.intro.intro.intro.inr.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hw : ↑x = w
hv : ↑y = v
⊢ G.Adj ↑y ↑x ∧ ↑y ∈ s ∧ ↑x ∈ s

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ ∀ (x y : V), (∃ x_1 y_1, G.Adj ↑x_1 ↑y_1 ∧ (↑x_1 = x ∧ ↑y_1 = y ∨ ↑x_1 = y ∧ ↑y_1 = x)) ↔ G.Adj x y ∧ x ∈ s ∧ y ∈ s

Tactic:
intro v w

Result:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ (∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)) ↔ G.Adj v w ∧ v ∈ s ∧ w ∈ s

Proof state:
case mpr
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
hadj : G.Adj v w
hv : v ∈ s
hw : w ∈ s
⊢ ∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)

Tactic:
use ⟨v, hv⟩, ⟨w, hw⟩, hadj

Result:
case right
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
hadj : G.Adj v w
hv : v ∈ s
hw : w ∈ s
⊢ ↑⟨v, hv⟩ = v ∧ ↑⟨w, hw⟩ = w ∨ ↑⟨v, hv⟩ = w ∧ ↑⟨w, hw⟩ = v

Proof state:
case right
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
hadj : G.Adj v w
hv : v ∈ s
hw : w ∈ s
⊢ ↑⟨v, hv⟩ = v ∧ ↑⟨w, hw⟩ = w ∨ ↑⟨v, hv⟩ = w ∧ ↑⟨w, hw⟩ = v

Tactic:
tauto

Result:
no goals

Proof state:
case mpr
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s → ∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)

Tactic:
intro ⟨hadj, hv, hw⟩

Result:
case mpr
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
hadj : G.Adj v w
hv : v ∈ s
hw : w ∈ s
⊢ ∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)

Proof state:
case mp.intro.intro.intro.inr.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hw : ↑x = w
hv : ↑y = v
⊢ G.Adj ↑y ↑x ∧ ↑y ∈ s ∧ ↑x ∈ s

Tactic:
exact ⟨hadj.symm, y.prop, x.prop⟩

Result:
no goals

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ (∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)) ↔ G.Adj v w ∧ v ∈ s ∧ w ∈ s

Tactic:
constructor

Result:
case mp
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ (∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)) → G.Adj v w ∧ v ∈ s ∧ w ∈ s

case mpr
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s → ∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)

Proof state:
case mp
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
⊢ (∃ x y, G.Adj ↑x ↑y ∧ (↑x = v ∧ ↑y = w ∨ ↑x = w ∧ ↑y = v)) → G.Adj v w ∧ v ∈ s ∧ w ∈ s

Tactic:
rintro ⟨x, y, hadj, ⟨hv, hw⟩ | ⟨hw, hv⟩⟩

Result:
case mp.intro.intro.intro.inl.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hv : ↑x = v
hw : ↑y = w
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s

case mp.intro.intro.intro.inr.intro
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
x y : Subtype s
hadj : G.Adj ↑x ↑y
hw : ↑x = w
hv : ↑y = v
⊢ G.Adj v w ∧ v ∈ s ∧ w ∈ s