awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
rw : IsClosed[inst] U ∧ Preperfect U ↔ U = derivedSet U
rw₁ : derivedSet U ⊆ U ∧ Preperfect U ↔ U = derivedSet U
rw₂ : derivedSet U ⊆ U ∧ U ⊆ derivedSet U ↔ U = derivedSet U
rw₃ : derivedSet U = U ↔ U = derivedSet U
rw₄ rw₅ : U = derivedSet U ↔ U = derivedSet U
⊢ Perfect U ↔ U = derivedSet U

Tactic:
rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]

Premises used: isClosed_iff_derivedSet_subset, eq_comm, perfect_def, subset_antisymm_iff, preperfect_iff_subset_derivedSet
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
pos : ∀ (hu : U.Nontrivial), (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
neg : ∀ (hu : ¬U.Nontrivial), (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
by_cases hu : U.Nontrivial

Premises used: Set.Nontrivial
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
pos : IsClosed[inst] (derivedSet a)
pos₁ : IsClosed[inst] (derivedSet b)
pos₂ : U ⊆ derivedSet a ∪ derivedSet b
pos₃ : (U ∩ derivedSet a).Nonempty
pos₄ : (U ∩ derivedSet b).Nonempty
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
apply isPreconnected_closed_iff.mp hs

Premises used: Iff.mp, isPreconnected_closed_iff
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ IsClosed[inst] (derivedSet a)

Tactic:
simp
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ IsClosed[inst] (derivedSet b)

Tactic:
simp
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
trans : U ⊆ derivedSet U
trans₁ : derivedSet U ⊆ derivedSet a ∪ derivedSet b
⊢ U ⊆ derivedSet a ∪ derivedSet b

Tactic:
trans derivedSet U

Premises used: derivedSet
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ U ⊆ derivedSet U

Tactic:
apply hs.preperfect_of_nontrivial hu

Premises used: IsPreconnected.preperfect_of_nontrivial
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
rw : derivedSet U ⊆ derivedSet (a ∪ b)
⊢ derivedSet U ⊆ derivedSet a ∪ derivedSet b

Tactic:
rw [← derivedSet_union]

Premises used: derivedSet_union
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ derivedSet U ⊆ derivedSet (a ∪ b)

Tactic:
derivedSet_mono _ _ h

Premises used: derivedSet_mono
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ derivedSet U ⊆ derivedSet (a ∪ b)

Tactic:
exact derivedSet_mono _ _ h

Premises used: derivedSet_mono
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet a).Nonempty

Tactic:
ha
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet a).Nonempty

Tactic:
exact ha
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet b).Nonempty

Tactic:
hb
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet b).Nonempty

Tactic:
exact hb
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : ¬U.Nontrivial
neg : ∀ (x : X) (hx : U = {x}), (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
obtain ⟨x, hx⟩ := ha.left.exists_eq_singleton_or_nontrivial.resolve_right hu

Premises used: Set.Nonempty.exists_eq_singleton_or_nontrivial, Set.Nonempty.left, Or.resolve_right
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : ¬U.Nontrivial
x : X
hx : U = {x}
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
simp_all
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace 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 :
  { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X }.toSetoid =
    { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 : DiscreteQuotient X }.toSetoid
⊢ { 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:
α : 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
A : Set X
h : IsClopen A
x : X
pos : ∀ (hx : x ∈ A), IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))
neg : ∀ (hx : x ∉ A), IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))
⊢ IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))

Tactic:
by_cases hx : x ∈ A
-- 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
A : Set X
h : IsClopen A
x : X
hx : x ∈ A
⊢ IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))

Tactic:
simp [hx, h.1, h.2, ← compl_setOf]

Premises used: And.right, And.left, Set.compl_setOf
-- 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
A : Set X
h : IsClopen A
x : X
hx : x ∉ A
⊢ IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))

Tactic:
simp [hx, h.1, h.2, ← compl_setOf]

Premises used: And.right, And.left, Set.compl_setOf
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
⊢ ∀ (x : X), (S.toSetoid : X → X → Prop) x x

Tactic:
S.refl'

Premises used: Setoid.refl', DiscreteQuotient.toSetoid
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
x y : X
⊢ (S.toSetoid : X → X → Prop) x y → (S.toSetoid : X → X → Prop) y x

Tactic:
S.symm'

Premises used: DiscreteQuotient.toSetoid, Setoid.symm'
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
x y z : X
⊢ (S.toSetoid : X → X → Prop) x y → (S.toSetoid : X → X → Prop) y z → (S.toSetoid : X → X → Prop) x z

Tactic:
S.trans'

Premises used: DiscreteQuotient.toSetoid, Setoid.trans'
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ S.proj ⁻¹' {S.proj x} = setOf ((S.toSetoid : X → X → Prop) x)

Tactic:
Set.ext fun _ => eq_comm.trans Quotient.eq''

Premises used: Set.ext, Quotient.eq'', eq_comm, Iff.trans
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
⊢ Surjective S.proj

Tactic:
Quotient.mk''_surjective

Premises used: Quotient.mk''_surjective
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
⊢ IsQuotientMap S.proj

Tactic:
isQuotientMap_quot_mk

Premises used: DiscreteQuotient.proj, Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
⊢ Continuous[inst, _] S.proj

Tactic:
S.proj_isQuotientMap.continuous

Premises used: Topology.IsQuotientMap.continuous, DiscreteQuotient.proj_isQuotientMap
-- 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
x : X
rw : IsOpen[inst] (setOf ((S.toSetoid : X → X → Prop) x))
⊢ IsOpen (X := Quotient S.toSetoid) {S.proj x}

Tactic:
rw [← S.proj_isQuotientMap.isOpen_preimage, fiber_eq]

Premises used: DiscreteQuotient.fiber_eq, Topology.IsCoinducing.isOpen_preimage, DiscreteQuotient.proj_isQuotientMap, Topology.IsQuotientMap.isCoinducing
-- 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
x : X
⊢ IsOpen[inst] (setOf ((S.toSetoid : X → X → Prop) x))

Tactic:
S.isOpen_setOf_rel _

Premises used: DiscreteQuotient.isOpen_setOf_rel
-- 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
x : X
⊢ IsOpen[inst] (setOf ((S.toSetoid : X → X → Prop) x))

Tactic:
exact S.isOpen_setOf_rel _

Premises used: DiscreteQuotient.isOpen_setOf_rel
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
⊢ IsLocallyConstant S.proj

Tactic:
(IsLocallyConstant.iff_continuous S.proj).2 S.proj_continuous

Premises used: Iff.mpr, DiscreteQuotient.proj, DiscreteQuotient.proj_continuous, IsLocallyConstant.iff_continuous
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
A : Set (Quotient S.toSetoid)
⊢ IsClopen (S.proj ⁻¹' A)

Tactic:
(isClopen_discrete A).preimage S.proj_continuous

Premises used: isClopen_discrete, DiscreteQuotient.proj_continuous, IsClopen.preimage
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
A : Set (Quotient S.toSetoid)
⊢ IsOpen[inst] (S.proj ⁻¹' A)

Tactic:
(S.isClopen_preimage A).2

Premises used: DiscreteQuotient.isClopen_preimage, And.right
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
A : Set (Quotient S.toSetoid)
⊢ IsClosed[inst] (S.proj ⁻¹' A)

Tactic:
(S.isClopen_preimage A).1

Premises used: DiscreteQuotient.isClopen_preimage, And.left
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
x : X
rw : IsClopen (S.proj ⁻¹' {S.proj x})
⊢ IsClopen (setOf ((S.toSetoid : X → X → Prop) x))

Tactic:
rw [← fiber_eq]

Premises used: DiscreteQuotient.fiber_eq
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (S.proj ⁻¹' {S.proj x})

Tactic:
apply isClopen_preimage

Premises used: DiscreteQuotient.isClopen_preimage
-- 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 a : DiscreteQuotient X
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ ⦃x y : X⦄, (a.toSetoid : X → X → Prop) x y → ({ toSetoid := ⊤, isOpen_setOf_rel := ⋯ }.toSetoid : X → X → Prop) x y
⊢ a ≤ { toSetoid := ⊤, isOpen_setOf_rel := ⋯ }

Tactic:
tauto
-- 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 : Nonempty X
⊢ Nonempty.{u_2 + 1} (Quotient S.toSetoid)

Tactic:
Nonempty.map S.proj ‹_›

Premises used: DiscreteQuotient.proj, Nonempty.map
-- 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
a : Quotient (α := X) (toSetoid ⊤)
a_1 : X
b : Quotient (α := X) (toSetoid ⊤)
a_2 : X
⊢ Eq (α := Quotient (α := X) (toSetoid ⊤)) (Quot.mk (⇑⊤.toSetoid : X → X → Prop) a_1)
    (Quot.mk (⇑⊤.toSetoid : X → X → Prop) a_2)

Tactic:
Quotient.sound trivial

Premises used: trivial, Quotient.sound
-- 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
a : Quotient (α := X) (toSetoid ⊤)
a_1 : X
b : Quotient (α := X) (toSetoid ⊤)
a_2 : X
⊢ Eq (α := Quotient (α := X) (toSetoid ⊤)) (Quot.mk (⇑⊤.toSetoid : X → X → Prop) a_1)
    (Quot.mk (⇑⊤.toSetoid : X → X → Prop) a_2)

Tactic:
exact Quotient.sound trivial

Premises used: Quotient.sound
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
⊢ comap (ContinuousMap.id X) S = S

Tactic:
rfl

Premises used: DiscreteQuotient.comap, rfl
-- 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
g : C(Y, Z)
f : C(X, Y)
S : DiscreteQuotient Z
⊢ comap (g.comp f) S = comap f (comap g S)

Tactic:
rfl

Premises used: ContinuousMap.comp, DiscreteQuotient.comap, 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 B : DiscreteQuotient Y
h : A ≤ B
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ ⦃x y : X⦄, ((comap f A).toSetoid : X → X → Prop) x y → ((comap f B).toSetoid : X → X → Prop) x y
⊢ comap f A ≤ comap f B

Tactic:
tauto
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
h :
  ∀ (x : Quotient A.toSetoid) (a : X),
    ofLE ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a) = id (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
⊢ ofLE ⋯ = id

Tactic:
ext ⟨⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
x : Quotient A.toSetoid
a : X
⊢ ofLE ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a) = id (Quot.mk (⇑A.toSetoid : X → X → Prop) a)

Tactic:
rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
a : Quotient A.toSetoid
⊢ ofLE ⋯ a = a

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
mk :
  ∀ (a : X),
    ofLE h₂ (ofLE h₁ (Quot.mk (⇑A.toSetoid : X → X → Prop) a)) = ofLE ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
⊢ ofLE h₂ (ofLE h₁ x) = ofLE ⋯ x

Tactic:
rcases x with ⟨⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk (⇑A.toSetoid : X → X → Prop) a)) = ofLE ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a)

Tactic:
rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
⊢ ofLE h₂ ∘ ofLE h₁ = ofLE ⋯

Tactic:
funext <| ofLE_ofLE _ _

Premises used: DiscreteQuotient.ofLE_ofLE, funext
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
⊢ Continuous (ofLE h)

Tactic:
continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
x : X
⊢ ofLE h (A.proj x) = B.proj x

Tactic:
Quotient.sound' (B.refl _)

Premises used: Quotient.sound', DiscreteQuotient.proj, DiscreteQuotient.ofLE, Quot.map, Quotient.map', DiscreteQuotient.refl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
⊢ ofLE h ∘ A.proj = B.proj

Tactic:
funext <| ofLE_proj _

Premises used: DiscreteQuotient.ofLE_proj, funext
-- 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 : LocallyConnectedSpace X
x : X
⊢ IsOpen[inst] (connectedComponent x)

Tactic:
isOpen_connectedComponent (x := x)

Premises used: isOpen_connectedComponent
-- 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 : LocallyConnectedSpace X
x : X
h : setOf ((connectedComponentSetoid X : X → X → Prop) x) = connectedComponent x
⊢ IsOpen[inst] (setOf ((connectedComponentSetoid X : X → X → Prop) x))

Tactic:
convert! isOpen_connectedComponent (x := x)

Premises used: isOpen_connectedComponent
-- 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 : LocallyConnectedSpace X
x : X
h : ∀ (y : X), y ∈ setOf ((connectedComponentSetoid X : X → X → Prop) x) ↔ y ∈ connectedComponent x
⊢ setOf ((connectedComponentSetoid X : X → X → Prop) x) = connectedComponent x

Tactic:
ext y
-- 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 : LocallyConnectedSpace X
x y : X
⊢ y ∈ setOf ((connectedComponentSetoid X : X → X → Prop) x) ↔ y ∈ connectedComponent x

Tactic:
simpa only [connectedComponentSetoid, ← connectedComponent_eq_iff_mem] using eq_comm

Premises used: connectedComponent_eq_iff_mem, eq_comm, connectedComponentSetoid
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : LocallyConnectedSpace X
x y : X
⊢ Eq (α := Quotient (α := X) (toSetoid ⊥)) (proj ⊥ x) (proj ⊥ y) ↔ connectedComponent x = connectedComponent y

Tactic:
Quotient.eq''

Premises used: DiscreteQuotient.proj, Quotient.eq''
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y : X
⊢ Eq (α := Quotient (α := X) (toSetoid ⊥)) (proj ⊥ x) (proj ⊥ y) ↔ x = y

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ Injective.{u_2 + 1, u_2 + 1} (α := X) (β := Quotient (α := X) (toSetoid ⊥)) (proj ⊥)

Tactic:
fun _ _ => proj_bot_inj.1

Premises used: DiscreteQuotient.proj_bot_inj, Iff.mp, Function.Injective
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := X) (β := Quotient (α := X) (toSetoid ⊥)) (proj ⊥)

Tactic:
⟨proj_bot_injective, proj_surjective _⟩

Premises used: And.intro, Function.Bijective, DiscreteQuotient.proj_surjective, DiscreteQuotient.proj_bot_injective
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
⊢ LEComap (ContinuousMap.id X) A A

Tactic:
le_rfl

Premises used: le_rfl, DiscreteQuotient.LEComap
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A A' : DiscreteQuotient X
⊢ LEComap (ContinuousMap.id X) A A' ↔ A ≤ A'

Tactic:
Iff.rfl

Premises used: Iff.rfl, DiscreteQuotient.LEComap
-- 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
tauto tauto₁ tauto₂ : LEComap g B C → LEComap f A B → LEComap (g.comp f) A C
tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ tauto₁₁ tauto₁₂ tauto₁₃ :
  LEComap g B C →
    LEComap f A B → ∀ ⦃x y : X⦄, (A.toSetoid : X → X → Prop) x y → ((comap (g.comp f) C).toSetoid : X → X → Prop) x y
⊢ LEComap g B C → LEComap f A B → LEComap (g.comp f) A C

Tactic:
tauto
-- 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 B' : DiscreteQuotient Y
h : LEComap f A B
hA : A' ≤ A
hB : B ≤ B'
⊢ LEComap f A' B'

Tactic:
hA.trans <| h.trans <| comap_mono _ hB

Premises used: DiscreteQuotient.comap_mono, LE.le.trans, DiscreteQuotient.LEComap
-- 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 : DiscreteQuotient Y
cond : LEComap f A B
⊢ Continuous (map f cond)

Tactic:
continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- 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 : DiscreteQuotient Y
cond : LEComap f A B
⊢ map f cond ∘ A.proj = B.proj ∘ (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: DiscreteQuotient.proj, Quotient.map', DiscreteQuotient.map, 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 : DiscreteQuotient Y
cond : LEComap f A B
x : X
⊢ map f cond (A.proj x) = B.proj ((f : (a : X) → Y) x)

Tactic:
rfl

Premises used: DiscreteQuotient.proj, Quotient.map', DiscreteQuotient.map, rfl
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
h :
  ∀ (x : Quotient A.toSetoid) (a : X),
    map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a) = id (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
⊢ map (ContinuousMap.id X) ⋯ = id

Tactic:
ext ⟨⟩
-- Module: Mathlib.Topology.DiscreteQuotient
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
x : Quotient A.toSetoid
a : X
⊢ map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid : X → X → Prop) a) = id (Quot.mk (⇑A.toSetoid : X → X → Prop) a)

Tactic:
rfl