awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
x : β
hx : x ∈ f '' derivedSet A
⊢ x ∈ derivedSet (f '' A)
have hx₁ : ∃ (x_1 : X), AccPt x_1 (𝓟 A) ∧ f x_1 = x
Tactic: simp only [Set.mem_image, mem_derivedSet] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
x : β
hx : ∃ (x_1 : X), AccPt x_1 (𝓟 A) ∧ f x_1 = x
⊢ x ∈ derivedSet (f '' A)
have obtain : ∀ (y : X) (hy1 : AccPt y (𝓟 A)), f y ∈ derivedSet (f '' A)
Tactic: obtain ⟨y, hy1, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A)
have a : f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))
Tactic: convert! hy1.map hf1.continuousAt hf2
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ IsClosed[inst] A
have rw : ∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A
Tactic: rw [isClosed_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
⊢ a ∈ A
have by_contra! : ∀ (nh : a ∉ A), False
Tactic: by_contra! nh
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ False
have this : A = A \ {a}
Tactic: have : A = A \ {a} := by simp [nh]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False
have ha₁ : AccPt a (𝓟 A)
Tactic: rw [this, ← accPt_principal_iff_clusterPt] at ha
Cleared hypotheses: ha, nh, this
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
⊢ closure[inst] A = A ∪ derivedSet A
have h : ∀ (x : X), x ∈ closure[inst] A ↔ x ∈ A ∪ derivedSet A
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
⊢ derivedSet (closure[inst] A) = derivedSet A
have refine : ∀ (x : X) (hx : x ∈ derivedSet (closure[inst] A)), x ∈ derivedSet A
Tactic: refine le_antisymm (fun x hx => ?_) (derivedSet_mono _ _ subset_closure)
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : x ∈ derivedSet (closure[inst] A)
⊢ x ∈ derivedSet A
have rw : ∀ (hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty) ⦃i : Set X⦄,
  x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ A).Nonempty
Tactic: rw [mem_derivedSet, AccPt, (nhdsWithin_basis_open x {x}ᶜ).inf_principal_neBot_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
⊢ ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ A).Nonempty
have h : ∀ (u : Set X) (hu : x ∈ u ∧ IsOpen[inst] u) (this : (u ∩ {x}ᶜ ∩ closure[inst] A).Nonempty), (u ∩ {x}ᶜ ∩ A).Nonempty
Tactic: peel hx with u hu _
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
u : Set X
hu : x ∈ u ∧ IsOpen[inst] u
this : (u ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty
have hu_open : IsOpen[inst] u
Tactic: obtain ⟨-, hu_open⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
⊢ IsClosed[inst] (derivedSet A)
have rw : derivedSet (derivedSet (closure[inst] A)) ⊆ derivedSet (closure[inst] A)
Tactic: rw [← derivedSet_closure, isClosed_iff_derivedSet_subset]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
⊢ derivedSet (derivedSet (closure[inst] A)) ⊆ derivedSet (closure[inst] A)
have h : derivedSet (closure[inst] A) ⊆ closure[inst] A
Tactic: apply derivedSet_mono
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
⊢ Perfect U ↔ U = derivedSet U
have rw : IsClosed[inst] U ∧ Preperfect U ↔ U = derivedSet U
Tactic: rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
rw : IsClosed[inst] U ∧ Preperfect U ↔ U = derivedSet U
⊢ Perfect U ↔ U = derivedSet U
have rw₁ : derivedSet U ⊆ U ∧ Preperfect U ↔ U = derivedSet U
Tactic: rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ Perfect U ↔ U = derivedSet U
have rw₂ : derivedSet U ⊆ U ∧ U ⊆ derivedSet U ↔ U = derivedSet U
Tactic: rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ Perfect U ↔ U = derivedSet U
have rw₃ : derivedSet U = U ↔ U = derivedSet U
Tactic: rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ Perfect U ↔ U = derivedSet U
have rw₄ : U = derivedSet U ↔ U = derivedSet U
Tactic: rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
have pos : ∀ (hu : U.Nontrivial), (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
Tactic: by_cases hu : U.Nontrivial
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
have neg : ∀ (hu : ¬U.Nontrivial), (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
Tactic: by_cases hu : U.Nontrivial
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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 ∩ derivedSet b)).Nonempty
have pos : IsClosed[inst] (derivedSet a)
Tactic: apply isPreconnected_closed_iff.mp hs
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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)
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
have pos₁ : IsClosed[inst] (derivedSet b)
Tactic: apply isPreconnected_closed_iff.mp hs
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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)
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
have pos₂ : U ⊆ derivedSet a ∪ derivedSet b
Tactic: apply isPreconnected_closed_iff.mp hs
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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 ∪ derivedSet b
have trans : U ⊆ derivedSet U
Tactic: trans derivedSet U
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ U ⊆ derivedSet a ∪ derivedSet b
have trans₁ : derivedSet U ⊆ derivedSet a ∪ derivedSet b
Tactic: trans derivedSet U
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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 ∪ derivedSet b
have rw : derivedSet U ⊆ derivedSet (a ∪ b)
Tactic: rw [← derivedSet_union]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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 ∩ derivedSet b)).Nonempty
have neg : ∀ (x : X) (hx : U = {x}), (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
Tactic: obtain ⟨x, hx⟩ := ha.left.exists_eq_singleton_or_nontrivial.resolve_right hu
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))
have pos : ∀ (hx : x ∈ A), IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))
Tactic: by_cases hx : x ∈ A
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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))
⊢ IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))
have neg : ∀ (hx : x ∉ A), IsOpen[inst] (setOf ((fun (x y : X) ↦ x ∈ A ↔ y ∈ A) x))
Tactic: by_cases hx : x ∈ A
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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 (X := Quotient S.toSetoid) {S.proj x}
have rw : IsOpen[inst] (setOf ((S.toSetoid : X → X → Prop) x))
Tactic: rw [← S.proj_isQuotientMap.isOpen_preimage, fiber_eq]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (setOf ((S.toSetoid : X → X → Prop) x))
have rw : IsClopen (S.proj ⁻¹' {S.proj x})
Tactic: rw [← fiber_eq]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ a ≤ { toSetoid := ⊤, isOpen_setOf_rel := ⋯ }
have tauto : ∀ ⦃x y : X⦄, (a.toSetoid : X → X → Prop) x y → ({ toSetoid := ⊤, isOpen_setOf_rel := sorry }.toSetoid : X → X → Prop) x y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ comap f A ≤ comap f B
have tauto : ∀ ⦃x y : X⦄, ((comap f A).toSetoid : X → X → Prop) x y → ((comap f B).toSetoid : X → X → Prop) x y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
⊢ ofLE ⋯ = id
have h : ∀ (x : Quotient A.toSetoid) (a : X),
  ofLE sorry (Quot.mk (⇑A.toSetoid : X → X → Prop) a) = id (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE ⋯ x
have mk : ∀ (a : X), ofLE h₂ (ofLE h₁ (Quot.mk (⇑A.toSetoid : X → X → Prop) a)) = ofLE sorry (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
Tactic: rcases x with ⟨⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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] (setOf ((connectedComponentSetoid X : X → X → Prop) x))
have h : setOf ((connectedComponentSetoid X : X → X → Prop) x) = connectedComponent x
Tactic: convert! isOpen_connectedComponent (x := x)
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ setOf ((connectedComponentSetoid X : X → X → Prop) x) = connectedComponent x
have h : ∀ (y : X), y ∈ setOf ((connectedComponentSetoid X : X → X → Prop) x) ↔ y ∈ connectedComponent x
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ LEComap g B C → LEComap f A B → LEComap (g.comp f) A C
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : DiscreteQuotient X
⊢ map (ContinuousMap.id X) ⋯ = id
have h : ∀ (x : Quotient A.toSetoid) (a : X),
  map (ContinuousMap.id X) sorry (Quot.mk (⇑A.toSetoid : X → X → Prop) a) = id (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ map (g.comp f) ⋯ = map g h1 ∘ map f h2
have h : ∀ (x : Quotient A.toSetoid) (a : X),
  map (g.comp f) sorry (Quot.mk (⇑A.toSetoid : X → X → Prop) a) =
    (map g h1 ∘ map f h2) (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ ofLE h (map f cond a) = map f ⋯ a
have mk : ∀ (a : X),
  ofLE h (map f cond (Quot.mk (⇑A.toSetoid : X → X → Prop) a)) = map f sorry (Quot.mk (⇑A.toSetoid : X → X → Prop) a)
Tactic: rcases a with ⟨⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ map f cond (ofLE h c) = map f ⋯ c
have mk : ∀ (a : X),
  map f cond (ofLE h (Quot.mk (⇑A'.toSetoid : X → X → Prop) a)) = map f sorry (Quot.mk (⇑A'.toSetoid : X → X → Prop) a)
Tactic: rcases c with ⟨⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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
⊢ x = y
have rw : ∀ (i : { s : Set X // IsClopen s ∧ y ∈ s }), x ∈ (↑i : Set X)
Tactic: rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_isClopen,
    mem_iInter]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
⊢ A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {ofLE h a}
have rcases : ∀ (a : X), A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}
Tactic: rcases A.proj_surjective a with ⟨a, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}
have rw : setOf ((A.toSetoid : X → X → Prop) a) ⊆ setOf ((B.toSetoid : X → X → Prop) a)
Tactic: rw [fiber_eq, ofLE_proj, fiber_eq]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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 ⁻¹' {Qs x_1}
have rw : x.proj ⁻¹' {Qs x} ⊆ x_1.proj ⁻¹' {ofLE h (Qs x)}
Tactic: rw [← compat _ _ h]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (hypothesis)
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), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
have H₁ : ∀ (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 _ _
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
have 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
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 _
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (hypothesis)
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
⊢ Finite.{u_2 + 1} (Quotient S.toSetoid)
have this : CompactSpace.{u_2} (Quotient S.toSetoid)
Tactic: have : CompactSpace S := Quotient.compactSpace
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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)
⊢ Finite.{u_2 + 1} (Quotient S.toSetoid)
have rwa : ∀ (this : IsCompact.{u_2} (X := Quotient S.toSetoid) univ), Finite.{u_2 + 1} (Quotient S.toSetoid)
Tactic: rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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)
⊢ Finite.{u_2 + 1} (Quotient S.toSetoid)
have rwa₁ : ∀ (this : Set.Finite.{u_2} (α := Quotient S.toSetoid) univ), Finite.{u_2 + 1} (Quotient S.toSetoid)
Tactic: rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
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)
⊢ Finite.{u_2 + 1} (Quotient S.toSetoid)
have rwa₂ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace 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
have 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
Tactic: ext d