-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_map_iff_of_nontrivial {f : α ↪ β} {t : Set β} (ht : t.Nontrivial) :
    (G.map f).IsClique t ↔ ∃ (s : Set α), G.IsClique s ∧ f '' s = t

Proof state:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
⊢ ⇑f '' (⇑f ⁻¹' t) = t

Tactic:
rw [Set.image_preimage_eq_iff]

Result:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
⊢ t ⊆ Set.range ⇑f

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj x y

Tactic:
rwa [← hux, ← hvy]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : (⇑f '' x).Nontrivial
⊢ (SimpleGraph.map f G).IsClique (⇑f '' x)

Tactic:
exact hs.map

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : β
hxt : x ∈ t
y : β
hyt : y ∈ t
hyne : y ≠ x
⊢ x ∈ Set.range ⇑f

Tactic:
obtain ⟨u,v, -, rfl, rfl⟩ := h hyt hxt hyne

Result:
case refine_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
u v : α
hyt : f u ∈ t
hxt : f v ∈ t
hyne : f u ≠ f v
⊢ f v ∈ Set.range ⇑f

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : f u = f x
hvy : f v = f y
⊢ G.Adj x y

Tactic:
rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj x y

Proof state:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
⊢ t ⊆ Set.range ⇑f

Tactic:
intro x hxt

Result:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : β
hxt : x ∈ t
⊢ x ∈ Set.range ⇑f

Proof state:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
⊢ G.IsClique (⇑f ⁻¹' t)

Tactic:
rintro x (hx : f x ∈ t) y (hy : f y ∈ t) hne

Result:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
⊢ G.Adj x y

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (SimpleGraph.map f G).IsClique t ↔ ∃ s, G.IsClique s ∧ ⇑f '' s = t

Tactic:
refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
⊢ G.IsClique (⇑f ⁻¹' t)

case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
⊢ ⇑f '' (⇑f ⁻¹' t) = t

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
u v : α
hyt : f u ∈ t
hxt : f v ∈ t
hyne : f u ≠ f v
⊢ f v ∈ Set.range ⇑f

Tactic:
exact Set.mem_range_self _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
⊢ f x ≠ f y

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = t) → (SimpleGraph.map f G).IsClique t

Tactic:
rintro ⟨x, hs, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : (⇑f '' x).Nontrivial
⊢ (SimpleGraph.map f G).IsClique (⇑f '' x)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : β
hxt : x ∈ t
⊢ x ∈ Set.range ⇑f

Tactic:
obtain ⟨y,hyt, hyne⟩ := ht.exists_ne x

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : β
hxt : x ∈ t
y : β
hyt : y ∈ t
hyne : y ≠ x
⊢ x ∈ Set.range ⇑f

Proof state:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
⊢ G.Adj x y

Tactic:
obtain ⟨u,v, huv, hux, hvy⟩ := h hx hy (by simpa)

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map f G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : f u = f x
hvy : f v = f y
⊢ G.Adj x y