internlm/Lean-Github huggingface dataset:
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Tactic:
replace k := k.isTotallyDisconnected_univ
Proof state after:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : IsTotallyDisconnected Set.univ
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : IsTotallyDisconnected Set.univ
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Tactic:
unfold _root_.IsTotallyDisconnected at k
Proof state after:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Set.Subsingleton (↑f.hom ⁻¹' t)
Tactic:
apply k
Proof state after:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ↑f.hom ⁻¹' t ⊆ Set.univ

case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ↑f.hom ⁻¹' t ⊆ Set.univ

case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)
Tactic:
tauto
Proof state after:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected (↑f.hom ⁻¹' t)
Tactic:
apply IsPreconnected.preimage_of_open_map
Proof state after:
case isTotallyDisconnected_univ.hs.a.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected t

case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a.hs
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsPreconnected t

case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Tactic:
assumption
Proof state after:
case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a.hinj
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ Function.Injective ↑f.hom

case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Tactic:
assumption
Proof state after:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom

case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a.hsf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ t ⊆ Set.range ↑f.hom
Tactic:
tauto
Proof state after:
no goals
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case surj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
⊢ Function.Surjective ↑f.hom
Tactic:
apply (TopCat.homeoOfIso f).surjective
Proof state after:
no goals
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case inj'
X Y : TopCat
k : TotallyDisconnectedSpace ↑X
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
⊢ Function.Injective ↑f.hom
Tactic:
apply (TopCat.homeoOfIso f).injective
Proof state after:
no goals
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ IsOpenMap ↑f.hom
Tactic:
unfold IsOpenMap
Proof state after:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ∀ (U : Set ↑X), IsOpen U → IsOpen (↑f.hom '' U)
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
⊢ ∀ (U : Set ↑X), IsOpen U → IsOpen (↑f.hom '' U)
Tactic:
intro U hU
Proof state after:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
U : Set ↑X
hU : IsOpen U
⊢ IsOpen (↑f.hom '' U)
Theorem: TotallyDisconnectedSpace.ofIso
Proof state before:
case isTotallyDisconnected_univ.hs.a.hf
X Y : TopCat
f : X ≅ Y
surj' : Function.Surjective ↑f.hom
inj' : Function.Injective ↑f.hom
t : Set ↑Y
a✝ : t ⊆ Set.univ
ht₂ : IsPreconnected t
k : ∀ (t : Set ↑X), t ⊆ Set.univ → IsPreconnected t → Set.Subsingleton t
U : Set ↑X
hU : IsOpen U
⊢ IsOpen (↑f.hom '' U)
Tactic:
apply TopCat.isOpen_iso _ hU
Proof state after:
no goals
Theorem: Profinite.finiteCoproduct.hom_ext
Proof state before:
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
Tactic:
ext ⟨a,x⟩
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toCompHaus.toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Theorem: Profinite.finiteCoproduct.hom_ext
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toCompHaus.toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
specialize h a
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Theorem: Profinite.finiteCoproduct.hom_ext
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
apply_fun (fun q => q x) at h
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Theorem: Profinite.finiteCoproduct.hom_ext
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
exact h
Proof state after:
no goals
Theorem: Profinite.EffectiveEpiFamily.ιFun_continuous
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous (ιFun π)
Tactic:
apply Continuous.quotient_lift
Proof state after:
case h
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(π a) x
Theorem: Profinite.EffectiveEpiFamily.ιFun_continuous
Proof state before:
case h
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(π a) x
Tactic:
apply continuous_sigma
Proof state after:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(π a) x
Theorem: Profinite.EffectiveEpiFamily.ιFun_continuous
Proof state before:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(π a) x
Tactic:
intro a
Proof state after:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(π a) x
Theorem: Profinite.EffectiveEpiFamily.ιFun_continuous
Proof state before:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(π a) x
Tactic:
exact (π a).continuous
Proof state after:
no goals
Theorem: Profinite.EffectiveEpiFamily.ιFun_injective
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Function.Injective (ιFun π)
Tactic:
rintro ⟨⟨a,x⟩⟩ ⟨⟨b,y⟩⟩ (h : π _ _ = π _ _)
Proof state after:
case mk.mk.mk.mk
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Quot.mk Setoid.r { fst := a, snd := x } = Quot.mk Setoid.r { fst := b, snd := y }
Theorem: Profinite.EffectiveEpiFamily.ιFun_injective
Proof state before:
case mk.mk.mk.mk
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Quot.mk Setoid.r { fst := a, snd := x } = Quot.mk Setoid.r { fst := b, snd := y }
Tactic:
apply Quotient.sound'
Proof state after:
case mk.mk.mk.mk.a
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Setoid.r { fst := a, snd := x } { fst := b, snd := y }
Theorem: Profinite.EffectiveEpiFamily.ιFun_injective
Proof state before:
case mk.mk.mk.mk.a
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Setoid.r { fst := a, snd := x } { fst := b, snd := y }
Tactic:
refine ⟨pullback (π a) (π b), ⟨⟨x,y⟩,h⟩, pullback.fst _ _, pullback.snd _ _, ?_, rfl, rfl⟩
Proof state after:
case mk.mk.mk.mk.a
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst = pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst
Theorem: Profinite.EffectiveEpiFamily.ιFun_injective
Proof state before:
case mk.mk.mk.mk.a
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst = pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst
Tactic:
ext ⟨_, h⟩
Proof state after:
case mk.mk.mk.mk.a.w.mk
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h✝ : ↑(π a) x = ↑(π b) y
val✝ : ↑(X a).toCompHaus.toTop × ↑(X b).toCompHaus.toTop
h : val✝ ∈ {xy | ↑(π a) xy.fst = ↑(π b) xy.snd}
⊢ ↑(pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst) { val := val✝, property := h } =
    ↑(pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst) { val := val✝, property := h }
Theorem: Profinite.EffectiveEpiFamily.ιFun_injective
Proof state before:
case mk.mk.mk.mk.a.w.mk
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h✝ : ↑(π a) x = ↑(π b) y
val✝ : ↑(X a).toCompHaus.toTop × ↑(X b).toCompHaus.toTop
h : val✝ ∈ {xy | ↑(π a) xy.fst = ↑(π b) xy.snd}
⊢ ↑(pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst) { val := val✝, property := h } =
    ↑(pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst) { val := val✝, property := h }
Tactic:
exact h
Proof state after:
no goals
Theorem: Profinite.EffectiveEpiFamily.ιFun_surjective
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Function.Surjective (ιFun π)
Tactic:
intro b
Proof state after:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
b : ↑B.toCompHaus.toTop
⊢ ∃ a, ιFun π a = b
Theorem: Profinite.EffectiveEpiFamily.ιFun_surjective
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
b : ↑B.toCompHaus.toTop
⊢ ∃ a, ιFun π a = b
Tactic:
obtain ⟨a,x,h⟩ := surj b
Proof state after:
case intro.intro
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
b : ↑B.toCompHaus.toTop
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(π a) x = b
⊢ ∃ a, ιFun π a = b
Theorem: Profinite.EffectiveEpiFamily.ιFun_surjective
Proof state before:
case intro.intro
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
b : ↑B.toCompHaus.toTop
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(π a) x = b
⊢ ∃ a, ιFun π a = b
Tactic:
refine ⟨Quotient.mk _ ⟨a,x⟩, h⟩
Proof state after:
no goals
Theorem: Profinite.EffectiveEpiFamily.CompHaus.TotallyDisconnectedSpace_ofIsIso
Proof state before:
X✝¹ Y✝ B✝ : Profinite
f✝ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f : X ≅ Y
⊢ TotallyDisconnectedSpace ↑Y.toTop
Tactic:
have f : X.toTop ≅ Y.toTop
Proof state after:
case f
X✝¹ Y✝ B✝ : Profinite
f✝ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f : X ≅ Y
⊢ X.toTop ≅ Y.toTop

X✝¹ Y✝ B✝ : Profinite
f✝¹ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f✝ : X ≅ Y
f : X.toTop ≅ Y.toTop
⊢ TotallyDisconnectedSpace ↑Y.toTop
Theorem: Profinite.EffectiveEpiFamily.CompHaus.TotallyDisconnectedSpace_ofIsIso
Proof state before:
X✝¹ Y✝ B✝ : Profinite
f✝¹ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f✝ : X ≅ Y
f : X.toTop ≅ Y.toTop
⊢ TotallyDisconnectedSpace ↑Y.toTop
Tactic:
apply TotallyDisconnectedSpace.ofIso f
Proof state after:
no goals
Theorem: Profinite.EffectiveEpiFamily.CompHaus.TotallyDisconnectedSpace_ofIsIso
Proof state before:
case f
X✝¹ Y✝ B✝ : Profinite
f✝ : X✝¹ ⟶ B✝
g : Y✝ ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X✝ : α → Profinite
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
X Y : CompHaus
k : TotallyDisconnectedSpace ↑X.toTop
f : X ≅ Y
⊢ X.toTop ≅ Y.toTop
Tactic:
exact compHausToTop.mapIso f
Proof state after:
no goals
Theorem: Profinite.EffectiveEpiFamily.π'_comp_ι_hom
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ π' π surj a ≫ (ι₂Iso π surj).hom = π a
Tactic:
ext
Proof state after:
case w
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
x✝ : (forget Profinite).obj (X a)
⊢ ↑(π' π surj a ≫ (ι₂Iso π surj).hom) x✝ = ↑(π a) x✝