-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_map_finset_iff_of_nontrivial (ht : t.Nontrivial) :
    (G.map f).IsClique t ↔ ∃ (s : Finset α), G.IsClique s ∧ s.map f = t

Proof state:
case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) → (SimpleGraph.map f G).IsClique ↑t

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
ht : (map f s).Nontrivial
⊢ (SimpleGraph.map f G).IsClique ↑(map f s)

Proof state:
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Finset α
hs : G.IsClique ↑s
hst : ⇑f '' ↑s = ↑t
⊢ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
exact ⟨s,hs, Finset.coe_inj.1 (by simpa)⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (↑t).Nontrivial

Tactic:
simpa

Result:
no goals

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

Tactic:
rintro ⟨s, hs, hst⟩

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : ⇑f '' s = ↑t
⊢ ∃ s, G.IsClique ↑s ∧ map f s = t

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
ht : (map f s).Nontrivial
⊢ (SimpleGraph.map f G).IsClique ↑(map f s)

Tactic:
simpa using hs.map (f := f)

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map f G).IsClique ↑t → ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
rw [isClique_map_iff_of_nontrivial (by simpa)]

Result:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = ↑t) → ∃ s, G.IsClique ↑s ∧ map f s = t

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Finset α
hs : G.IsClique ↑s
hst : ⇑f '' ↑s = ↑t
⊢ ↑(map f s) = ↑t

Tactic:
simpa

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : ⇑f '' s = ↑t
⊢ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
obtain ⟨s, rfl⟩ := Set.Finite.exists_finset_coe <|
  (show s.Finite from Set.Finite.of_finite_image (by simp [hst]) f.injective.injOn)

Result:
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Finset α
hs : G.IsClique ↑s
hst : ⇑f '' ↑s = ↑t
⊢ ∃ s, G.IsClique ↑s ∧ map f s = t

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

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map f G).IsClique ↑t → ∃ s, G.IsClique ↑s ∧ map f s = t

case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) → (SimpleGraph.map f G).IsClique ↑t

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : ⇑f '' s = ↑t
⊢ (⇑f '' s).Finite

Tactic:
simp [hst]

Result:
no goals