-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueSet_map (hn : n ≠ 1) (G : SimpleGraph α) (f : α ↪ β) :
    (G.map f).cliqueSet n = map f '' G.cliqueSet n

Proof state:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ s ∈ map f '' G.cliqueSet #s

Tactic:
refine ⟨s.preimage f f.injective.injOn, ⟨?_, by rw [← card_map f, hs']⟩, hs'⟩

Result:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ G.IsClique ↑(s.preimage ⇑f ⋯)

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
⊢ map f (s.preimage ⇑f ⋯) = s

Tactic:
classical
rw [map_eq_image, image_preimage, filter_true_of_mem]
rintro a ha
obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
obtain ⟨c, _, _, hc, _⟩ := hs ha hb hba.symm
exact ⟨c, hc⟩

Result:
no goals

Proof state:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ G.IsClique ↑(s.preimage ⇑f ⋯)

Tactic:
rw [coe_preimage]

Result:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ G.IsClique (⇑f ⁻¹' ↑s)

Proof state:
case h
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map f G).cliqueSet n ↔ s ∈ map f '' G.cliqueSet n

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map f G).cliqueSet n → s ∈ map f '' G.cliqueSet n

case h.mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map f G).cliqueSet n

Proof state:
case h.mp
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map f G).cliqueSet n → s ∈ map f '' G.cliqueSet n

Tactic:
rintro ⟨hs, rfl⟩

Result:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
⊢ s ∈ map f '' G.cliqueSet #s

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
⊢ map f (s.preimage ⇑f ⋯) = s

Tactic:
rw [map_eq_image, image_preimage, filter_true_of_mem]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
⊢ ∀ x ∈ s, x ∈ Set.range ⇑f

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
⊢ a ∈ Set.range ⇑f

Tactic:
obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a

Result:
case intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
⊢ a ∈ Set.range ⇑f

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
c w✝ : α
left✝ : G.Adj c w✝
hc : f c = a
right✝ : f w✝ = b
⊢ a ∈ Set.range ⇑f

Tactic:
exact ⟨c, hc⟩

Result:
no goals

Proof state:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ G.IsClique (⇑f ⁻¹' ↑s)

Tactic:
exact fun a ha b hb hab => map_adj_apply.1 (hs ha hb <| f.injective.ne hab)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
⊢ ∀ x ∈ s, x ∈ Set.range ⇑f

Tactic:
rintro a ha

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
⊢ a ∈ Set.range ⇑f

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
⊢ (SimpleGraph.map f G).cliqueSet n = map f '' G.cliqueSet n

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ (SimpleGraph.map f G).cliqueSet n ↔ s ∈ map f '' G.cliqueSet n

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
⊢ s ∈ map f '' G.cliqueSet n → s ∈ (SimpleGraph.map f G).cliqueSet n

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : s ∈ G.cliqueSet n
⊢ map f s ∈ (SimpleGraph.map f G).cliqueSet n

Proof state:
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : s ∈ G.cliqueSet n
⊢ map f s ∈ (SimpleGraph.map f G).cliqueSet n

Tactic:
exact hs.map

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ #(s.preimage ⇑f ⋯) = #s

Tactic:
rw [← card_map f, hs']

Result:
no goals

Proof state:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
⊢ s ∈ map f '' G.cliqueSet #s

Tactic:
have hs' : (s.preimage f f.injective.injOn).map f = s := by
  classical
  rw [map_eq_image, image_preimage, filter_true_of_mem]
  rintro a ha
  obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
  obtain ⟨c, _, _, hc, _⟩ := hs ha hb hba.symm
  exact ⟨c, hc⟩

Result:
case h.mp.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ s ∈ map f '' G.cliqueSet #s

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
⊢ a ∈ Set.range ⇑f

Tactic:
obtain ⟨c, _, _, hc, _⟩ := hs ha hb hba.symm

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map f G).IsClique ↑s
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
c w✝ : α
left✝ : G.Adj c w✝
hc : f c = a
right✝ : f w✝ = b
⊢ a ∈ Set.range ⇑f