Theorem: SimpleGraph.Subgraph.edgeSet_map (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
⊢ (Subgraph.map f G').edgeSet = Sym2.map ⇑f '' G'.edgeSet
Tactic:
ext e
State after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
e : Sym2 β
⊢ e ∈ (Subgraph.map f G').edgeSet ↔ e ∈ Sym2.map ⇑f '' G'.edgeSet

State before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
e : Sym2 β
⊢ e ∈ (Subgraph.map f G').edgeSet ↔ e ∈ Sym2.map ⇑f '' G'.edgeSet
Tactic:
induction' e using Sym2.ind with a b
State after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ s(a, b) ∈ (Subgraph.map f G').edgeSet ↔ s(a, b) ∈ Sym2.map ⇑f '' G'.edgeSet

State before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ s(a, b) ∈ (Subgraph.map f G').edgeSet ↔ s(a, b) ∈ Sym2.map ⇑f '' G'.edgeSet
Tactic:
simp only [mem_edgeSet, Sym2.exists, Relation.Map, and_or_left, exists_or, map_adj,
  Set.mem_image, Sym2.map_pair_eq, Sym2.eq, Sym2.rel_iff]
State after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ↔
    (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∨ ∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a

State before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ↔
    (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∨ ∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a
Tactic:
refine' (or_iff_left_of_imp _).symm
State after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a) → ∃ a_2 b_1, G'.Adj a_2 b_1 ∧ f a_2 = a ∧ f b_1 = b

State before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a) → ∃ a_2 b_1, G'.Adj a_2 b_1 ∧ f a_2 = a ∧ f b_1 = b
Tactic:
rintro ⟨a, b, hab, rfl, rfl⟩
State after:
case h.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : α
hab : G'.Adj a b
⊢ ∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = f b ∧ f b_1 = f a

State before:
case h.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : α
hab : G'.Adj a b
⊢ ∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = f b ∧ f b_1 = f a
Tactic:
exact ⟨b, a, hab.symm, rfl, rfl⟩
State after:
no goals