-- Mathlib/Order/Filter/CountableSeparatingOn.lean
theorem HasCountableSeparatingOn.subtype_iff {α : Type*} {p : Set α → Prop} {t : Set α} :
    HasCountableSeparatingOn t (fun u ↦ ∃ v, p v ∧ (↑) ⁻¹' v = u) univ ↔
    HasCountableSeparatingOn α p t

Proof state:
case mp
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn α p t

Tactic:
exact h.of_subtype <| fun s ↦ id

Result:
no goals

Proof state:
case right
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, x ∈ s ↔ y ∈ s) → x = y

Tactic:
rintro x - y - hxy

Result:
case right
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : ↑t
hxy : ∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, x ∈ s ↔ y ∈ s
⊢ x = y

Proof state:
case mpr.mk.intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ

Tactic:
use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_

Result:
case left
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, ∃ v, p v ∧ Subtype.val ⁻¹' v = s

case right
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, x ∈ s ↔ y ∈ s) → x = y

Proof state:
case right
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : ↑t
hxy : ∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, x ∈ s ↔ y ∈ s
⊢ x = y

Tactic:
exact Subtype.val_injective <| hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _)
  fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ

Tactic:
rcases h with ⟨S, Sct, Sp, hS⟩

Result:
case mpr.mk.intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ

Proof state:
case left.intro.intro
α : Type u_1
p : Set α → Prop
t✝ : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t✝, ∀ y ∈ t✝, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
t : Set α
tS : t ∈ S
⊢ ∃ v, p v ∧ Subtype.val ⁻¹' v = Subtype.val ⁻¹' t

Tactic:
exact ⟨t, Sp _ tS, rfl⟩

Result:
no goals

Proof state:
case left
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, ∃ v, p v ∧ Subtype.val ⁻¹' v = s

Tactic:
rintro u ⟨t, tS, rfl⟩

Result:
case left.intro.intro
α : Type u_1
p : Set α → Prop
t✝ : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t✝, ∀ y ∈ t✝, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
t : Set α
tS : t ∈ S
⊢ ∃ v, p v ∧ Subtype.val ⁻¹' v = Subtype.val ⁻¹' t

Proof state:
α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ ↔ HasCountableSeparatingOn α p t

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
⊢ HasCountableSeparatingOn α p t

case mpr
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ