-- Mathlib/Topology/DiscreteQuotient.lean
/-- A helper lemma to prove that `finsetClopens X` is injective, see `finsetClopens_inj`. -/
lemma comp_finsetClopens [CompactSpace X] :
    (Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ Finset.toSet) ∘
      finsetClopens X = fun ⟨f, _⟩ ↦ f.classes

Proof state:
case h.h.mp.h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ a, d.proj ⁻¹' {a} = x✝²
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝²
x✝ : X
⊢ x✝ ∈ x✝² ↔ x✝ ∈ {x | d.toSetoid x y.out}

Tactic:
simpa [← h] using Quotient.mk_eq_iff_out (s := d.toSetoid)

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ ((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X = fun x =>
    match x with
    | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

Tactic:
ext d

Result:
case h.h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ x✝ ∈ (((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X) d ↔
    x✝ ∈
      match d with
      | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

Proof state:
case h.h.mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) → ∃ y, x✝ = {x | d.toSetoid x y}

Tactic:
refine fun ⟨y, h⟩ ↦ ⟨Quotient.out (s := d.toSetoid) y, ?_⟩

Result:
case h.h.mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ a, d.proj ⁻¹' {a} = x✝¹
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝¹
⊢ x✝¹ = {x | d.toSetoid x y.out}

Proof state:
case h.h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) ↔ ∃ y, x✝ = {x | d.toSetoid x y}

Tactic:
constructor

Result:
case h.h.mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) → ∃ y, x✝ = {x | d.toSetoid x y}

case h.h.mpr
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ y, x✝ = {x | d.toSetoid x y}) → ∃ a, d.proj ⁻¹' {a} = x✝

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ y, x✝¹ = {x | d.toSetoid x y}
y : X
h : x✝¹ = {x | d.toSetoid x y}
⊢ d.proj ⁻¹' {d.proj y} = x✝¹

Tactic:
ext

Result:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ y, x✝² = {x | d.toSetoid x y}
y : X
h : x✝² = {x | d.toSetoid x y}
x✝ : X
⊢ x✝ ∈ d.proj ⁻¹' {d.proj y} ↔ x✝ ∈ x✝²

Proof state:
case h.h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ x✝ ∈ (((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X) d ↔
    x✝ ∈
      match d with
      | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

Tactic:
simp only [Setoid.classes, Set.mem_setOf_eq, Function.comp_apply,
  finsetClopens, Set.coe_toFinset, Set.mem_image, Set.mem_range,
  exists_exists_eq_and]

Result:
case h.h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) ↔ ∃ y, x✝ = {x | d.toSetoid x y}

Proof state:
case h.h.mpr
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ y, x✝ = {x | d.toSetoid x y}) → ∃ a, d.proj ⁻¹' {a} = x✝

Tactic:
exact fun ⟨y, h⟩ ↦ ⟨d.proj y, by ext; simp [h, proj]⟩

Result:
no goals

Proof state:
case h.h.mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ a, d.proj ⁻¹' {a} = x✝¹
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝¹
⊢ x✝¹ = {x | d.toSetoid x y.out}

Tactic:
ext

Result:
case h.h.mp.h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ a, d.proj ⁻¹' {a} = x✝²
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝²
x✝ : X
⊢ x✝ ∈ x✝² ↔ x✝ ∈ {x | d.toSetoid x y.out}

Proof state:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ y, x✝² = {x | d.toSetoid x y}
y : X
h : x✝² = {x | d.toSetoid x y}
x✝ : X
⊢ x✝ ∈ d.proj ⁻¹' {d.proj y} ↔ x✝ ∈ x✝²

Tactic:
simp [h, proj]

Result:
no goals