-- Mathlib/Topology/DiscreteQuotient.lean
theorem finsetClopens_inj [CompactSpace X] :
    (finsetClopens X).Injective

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (finsetClopens X)

Tactic:
apply Function.Injective.of_comp (f := Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ Finset.toSet)

Result:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X)

Proof state:
case e_toSetoid
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
h :
  (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
⊢ toSetoid✝¹.classes = toSetoid✝.classes

Tactic:
exact h

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X)

Tactic:
rw [comp_finsetClopens]

Result:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective fun x =>
    match x with
    | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

Proof state:
case e_toSetoid
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
h :
  (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
⊢ toSetoid✝¹ = toSetoid✝

Tactic:
rw [Setoid.classes_inj]

Result:
case e_toSetoid
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
h :
  (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
⊢ toSetoid✝¹.classes = toSetoid✝.classes

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective fun x =>
    match x with
    | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

Tactic:
intro ⟨_, _⟩ ⟨_, _⟩ h

Result:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
h :
  (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
⊢ { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
h :
  (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
⊢ { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }

Tactic:
congr

Result:
case e_toSetoid
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
h :
  (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    (fun x =>
        match x with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
⊢ toSetoid✝¹ = toSetoid✝