awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
h :
  ∀ (x : Quotient A.toSetoid) (a : X),
    map (g.comp f) ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a) =
      (map g h1 ∘ map f h2) (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
⊢ map (g.comp f) ⋯ = map g h1 ∘ map f h2

Tactic:
ext ⟨⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
x : Quotient A.toSetoid
a : X
⊢ map (g.comp f) ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a) =
    (map g h1 ∘ map f h2) (Quot.mk (⇑A.toSetoid : X → X → Prop) a)

Tactic:
rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
mk :
  ∀ (a : X),
    ofLE h (map f cond (Quot.mk (⇑A.toSetoid : X → X → Prop) a)) = map f ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
⊢ ofLE h (map f cond a) = map f ⋯ a

Tactic:
rcases a with ⟨⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a_1 : X
⊢ ofLE h (map f cond (Quot.mk (⇑A.toSetoid : X → X → Prop) a_1)) = map f ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a_1)

Tactic:
rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
⊢ ofLE h ∘ map f cond = map f ⋯

Tactic:
funext <| ofLE_map cond h

Premises used: DiscreteQuotient.ofLE_map, funext
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
mk :
  ∀ (a : X),
    map f cond (ofLE h (Quot.mk (⇑A'.toSetoid : X → X → Prop) a)) = map f ⋯ (Quot.mk (⇑A'.toSetoid : X → X → Prop) a)
⊢ map f cond (ofLE h c) = map f ⋯ c

Tactic:
rcases c with ⟨⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a : X
⊢ map f cond (ofLE h (Quot.mk (⇑A'.toSetoid : X → X → Prop) a)) = map f ⋯ (Quot.mk (⇑A'.toSetoid : X → X → Prop) a)

Tactic:
rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
⊢ map f cond ∘ ofLE h = map f ⋯

Tactic:
funext <| map_ofLE cond h

Premises used: funext, DiscreteQuotient.map_ofLE
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
rw : ∀ (i : { s : Set X // IsClopen s ∧ y ∈ s }), x ∈ (↑i : Set X)
⊢ x = y

Tactic:
rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_isClopen,
    mem_iInter]

Premises used: connectedComponent_eq_singleton, Set.mem_iInter, Set.mem_singleton_iff, connectedComponent_eq_iInter_isClopen
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
U : Set X
hU1 : IsClopen U
hU2 : y ∈ U
⊢ x ∈ (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ y ∈ s) U ⋯) : Set X)

Tactic:
(Quotient.exact' (h (ofIsClopen hU1))).mpr hU2

Premises used: Iff.mpr, Set.Mem, Quotient.exact', DiscreteQuotient.ofIsClopen
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
U : Set X
hU1 : IsClopen U
hU2 : y ∈ U
⊢ x ∈ (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ y ∈ s) U ⋯) : Set X)

Tactic:
exact (Quotient.exact' (h (ofIsClopen hU1))).mpr hU2

Premises used: Iff.mpr, Quotient.exact', DiscreteQuotient.ofIsClopen
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
rcases : ∀ (a : X), A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}
⊢ A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {ofLE h a}

Tactic:
rcases A.proj_surjective a with ⟨a, rfl⟩

Premises used: DiscreteQuotient.proj_surjective, rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
rw : setOf ((A.toSetoid : X → X → Prop) a) ⊆ setOf ((B.toSetoid : X → X → Prop) a)
⊢ A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}

Tactic:
rw [fiber_eq, ofLE_proj, fiber_eq]

Premises used: DiscreteQuotient.ofLE_proj, DiscreteQuotient.fiber_eq
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf ((A.toSetoid : X → X → Prop) a) ⊆ setOf ((B.toSetoid : X → X → Prop) a)

Tactic:
fun _ h' => h h'

Premises used: Set.Mem, setOf, Set.Subset
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf ((A.toSetoid : X → X → Prop) a) ⊆ setOf ((B.toSetoid : X → X → Prop) a)

Tactic:
exact fun _ h' => h h'
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x x_1 : DiscreteQuotient X
h : x ≤ x_1
rw : x.proj ⁻¹' {Qs x} ⊆ x_1.proj ⁻¹' {ofLE h (Qs x)}
⊢ x.proj ⁻¹' {Qs x} ⊆ x_1.proj ⁻¹' {Qs x_1}

Tactic:
rw [← compat _ _ h]
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x x_1 : DiscreteQuotient X
h : x ≤ x_1
⊢ x.proj ⁻¹' {Qs x} ⊆ x_1.proj ⁻¹' {ofLE h (Qs x)}

Tactic:
fiber_subset_ofLE _ _

Premises used: DiscreteQuotient.fiber_subset_ofLE
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x x_1 : DiscreteQuotient X
h : x ≤ x_1
⊢ x.proj ⁻¹' {Qs x} ⊆ x_1.proj ⁻¹' {ofLE h (Qs x)}

Tactic:
exact fiber_subset_ofLE _ _

Premises used: DiscreteQuotient.fiber_subset_ofLE
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
⊢ ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}

Tactic:
have H₁ : ∀ Q₁ Q₂, Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂} := fun _ _ h => by
    rw [← compat _ _ h]
    exact fiber_subset_ofLE _ _
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}
⊢ Set.Nonempty.{u_2} (α := X) (⋂ (Q : DiscreteQuotient X), Q.proj ⁻¹' {Qs Q})

Tactic:
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
      (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _}) (directed_of_isDirected_ge H₁)
      (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
      (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _

Premises used: Set.singleton_nonempty, DiscreteQuotient.proj, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, Set.preimage, DiscreteQuotient.isClosed_preimage, IsClosed.isCompact, Set.Nonempty.preimage, DiscreteQuotient.proj_surjective, Singleton.singleton, directed_of_isDirected_ge
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}
obtain :
  ∀ (x : X) (hx : Membership.mem (γ := Set X) (⋂ (Q : DiscreteQuotient X), Q.proj ⁻¹' {Qs Q}) x),
    ∃ (x : X), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
⊢ ∃ (x : X), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Tactic:
obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
      (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _}) (directed_of_isDirected_ge H₁)
      (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
      (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _

Premises used: Set.singleton_nonempty, DiscreteQuotient.proj, Set.iInter, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, Set.Nonempty, Set.preimage, DiscreteQuotient.isClosed_preimage, IsClosed.isCompact, Set.Nonempty.preimage, DiscreteQuotient.proj_surjective, Singleton.singleton, directed_of_isDirected_ge
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}
x : X
hx : Membership.mem (γ := Set X) (⋂ (Q : DiscreteQuotient X), Q.proj ⁻¹' {Qs Q}) x
⊢ ∃ (x : X), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Tactic:
⟨x, mem_iInter.1 hx⟩

Premises used: Set.mem_iInter, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}
x : X
hx : Membership.mem (γ := Set X) (⋂ (Q : DiscreteQuotient X), Q.proj ⁻¹' {Qs Q}) x
⊢ ∃ (x : X), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Tactic:
exact ⟨x, mem_iInter.1 hx⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
S : DiscreteQuotient X
inst_3 : CompactSpace X
⊢ CompactSpace.{u_2} (Quotient S.toSetoid)

Tactic:
have : CompactSpace S := Quotient.compactSpace
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
S : DiscreteQuotient X
inst_3 : CompactSpace X
this : CompactSpace.{u_2} (Quotient S.toSetoid)
rwa : ∀ (this : IsCompact.{u_2} (X := Quotient S.toSetoid) univ), Finite.{u_2 + 1} (Quotient S.toSetoid)
rwa₁ : ∀ (this : Set.Finite.{u_2} (α := Quotient S.toSetoid) univ), Finite.{u_2 + 1} (Quotient S.toSetoid)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : Finite.{u_2 + 1} (Quotient S.toSetoid)), Finite.{u_2 + 1} (Quotient S.toSetoid)
⊢ Finite.{u_2 + 1} (Quotient S.toSetoid)

Tactic:
rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this

Premises used: isCompact_iff_finite, isCompact_univ_iff, Set.finite_univ_iff
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
h :
  ∀ (d : DiscreteQuotient X) (x : Set X),
    Membership.mem (γ := Set (Set X)) ((((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X) d)
        x ↔
      Membership.mem (γ := Set (Set X))
        (match (motive := DiscreteQuotient X → Set (Set X)) d with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X))
        x
⊢ Eq (α := DiscreteQuotient X → Set (Set X)) (((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)
    fun (x : DiscreteQuotient X) ↦
    match (motive := DiscreteQuotient X → Set (Set X)) x with
    | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

Tactic:
ext d
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h : (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) ↔ ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
⊢ Membership.mem (γ := Set (Set X)) ((((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X) d) x ↔
    Membership.mem (γ := Set (Set X))
      (match (motive := DiscreteQuotient X → Set (Set X)) d with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
        Set (Set X))
      x

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]

Premises used: Set.mem_range, Set.mem_image, Setoid.classes, Set.mem_setOf_eq, DiscreteQuotient.finsetClopens, exists_exists_eq_and, Function.comp_apply, Set.coe_toFinset
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h : (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) → ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
h₁ : (∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}) → ∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x
⊢ (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) ↔ ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}

Tactic:
constructor
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
⊢ (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) → ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}

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

Premises used: setOf, Exists, _private.0.DiscreteQuotient.comp_finsetClopens.match_6, Quotient.out, Exists.intro, Eq, Setoid.r
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h :
  (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) →
    ∀ (y : Quotient d.toSetoid) (h : d.proj ⁻¹' {y} = x), x = {x : X | (d.toSetoid : X → X → Prop) x y.out}
⊢ (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) → ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}

Tactic:
refine fun ⟨y, h⟩ ↦ ⟨Quotient.out (s := d.toSetoid) y, ?_⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h_1 : ∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x
h₁ : ∀ (x_1 : X), x_1 ∈ x ↔ Membership.mem (γ := Set X) {x : X | (d.toSetoid : X → X → Prop) x y.out} x_1
⊢ x = {x : X | (d.toSetoid : X → X → Prop) x y.out}

Tactic:
ext
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h_1 : ∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x
x_1 : X
⊢ x_1 ∈ x ↔ Membership.mem (γ := Set X) {x : X | (d.toSetoid : X → X → Prop) x y.out} x_1

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

Premises used: Quotient.mk_eq_iff_out
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h_1 : ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
y : X
h : x = {x : X | (d.toSetoid : X → X → Prop) x y}
h₁ : ∀ (x_1 : X), x_1 ∈ d.proj ⁻¹' {d.proj y} ↔ x_1 ∈ x
⊢ d.proj ⁻¹' {d.proj y} = x

Tactic:
ext
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h_1 : ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
y : X
h : x = {x : X | (d.toSetoid : X → X → Prop) x y}
x_1 : X
⊢ x_1 ∈ d.proj ⁻¹' {d.proj y} ↔ x_1 ∈ x

Tactic:
simp [h, proj, Quotient.eq]

Premises used: DiscreteQuotient.proj, Quotient.eq
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
⊢ (∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}) → ∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x

Tactic:
exact fun ⟨y, h⟩ ↦ ⟨d.proj y, by ext; simp [h, proj, Quotient.eq]⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
apply :
  Injective (α := DiscreteQuotient X) (β := Set (Set X))
    (((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)
⊢ Injective (α := DiscreteQuotient X) (finsetClopens X)

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

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
rw :
  Injective (β := Set (Set X)) fun (x : DiscreteQuotient X) ↦
    match (motive := DiscreteQuotient X → Set (Set X)) x with
    | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes
⊢ Injective (α := DiscreteQuotient X) (β := Set (Set X))
    (((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)

Tactic:
rw [comp_finsetClopens]

Premises used: DiscreteQuotient.comp_finsetClopens
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
this :
  ∀ (toSetoid_1 : Setoid X) (isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))),
    Eq.{u_2 + 1} (α := Set (Set X))
        ((fun (x : DiscreteQuotient X) ↦
            (match (motive := DiscreteQuotient X → Set (Set X)) x with
              | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
              Set (Set X)))
          { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
        ((fun (x : DiscreteQuotient X) ↦
            (match (motive := DiscreteQuotient X → Set (Set X)) x with
              | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
              Set (Set X)))
          { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 }) →
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X } =
        { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 }
⊢ ∀ ⦃a₂ : DiscreteQuotient X⦄,
    Eq.{u_2 + 1} (α := Set (Set X))
        ((fun (x : DiscreteQuotient X) ↦
            (match (motive := DiscreteQuotient X → Set (Set X)) x with
              | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
              Set (Set X)))
          { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
        ((fun (x : DiscreteQuotient X) ↦
            (match (motive := DiscreteQuotient X → Set (Set X)) x with
              | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
              Set (Set X)))
          a₂) →
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X } = a₂

Tactic:
⟨_, _⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
toSetoid_1 : Setoid X
isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))
h :
  Eq.{u_2 + 1} (α := Set (Set X))
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 })
e_toSetoid : toSetoid = toSetoid_1
⊢ { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X } =
    { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 }

Tactic:
congr
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
toSetoid_1 : Setoid X
isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))
h :
  Eq.{u_2 + 1} (α := Set (Set X))
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 })
e_toSetoid : toSetoid.classes = toSetoid_1.classes
⊢ toSetoid = toSetoid_1

Tactic:
rw [Setoid.classes_inj]

Premises used: Setoid.classes_inj
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
toSetoid_1 : Setoid X
isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))
h :
  Eq.{u_2 + 1} (α := Set (Set X))
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 })
⊢ toSetoid.classes = toSetoid_1.classes

Tactic:
h