internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
⊢ ∀ (U_1 : Set ↑U), IsOpen U_1 → IsOpen (closure U_1)
Tactic:
intro V hV
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
⊢ IsOpen (closure V)
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
⊢ IsOpen (closure V)
Tactic:
have hV' : IsOpen (Subtype.val '' V) := hU.1.openEmbedding_subtype_val.isOpenMap V hV
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
⊢ IsOpen (closure V)
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
⊢ IsOpen (closure V)
Tactic:
have := ExtremallyDisconnected.open_closure _ hV'
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (closure (Subtype.val '' V))
⊢ IsOpen (closure V)
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (closure (Subtype.val '' V))
⊢ IsOpen (closure V)
Tactic:
rw [hU.2.closedEmbedding_subtype_val.closure_image_eq V] at this
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ IsOpen (closure V)
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ IsOpen (closure V)
Tactic:
suffices hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' (closure V))
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (closure V)

case hhU
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case hhU
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
⊢ closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
Tactic:
exact ((closure V).preimage_image_eq Subtype.coe_injective).symm
Proof state after:
no goals
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (closure V)
Tactic:
rw [hhU]
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (Subtype.val ⁻¹' (Subtype.val '' closure V))
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
V : Set ↑U
hV : IsOpen V
hV' : IsOpen (Subtype.val '' V)
this : IsOpen (Subtype.val '' closure V)
hhU : closure V = Subtype.val ⁻¹' (Subtype.val '' closure V)
⊢ IsOpen (Subtype.val ⁻¹' (Subtype.val '' closure V))
Tactic:
exact isOpen_induced this
Proof state after:
no goals
Theorem: CategoryTheory.aux_forall_mem
Proof state before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ ∀ (x : ↑(↑f ⁻¹' Set.range ↑i)), ↑f ↑x ∈ Set.range ↑i
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case mk
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
x : CoeSort.coe X
hx : x ∈ ↑f ⁻¹' Set.range ↑i
⊢ ↑f ↑{ val := x, property := hx } ∈ Set.range ↑i
Theorem: CategoryTheory.aux_forall_mem
Proof state before:
case mk
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
x : CoeSort.coe X
hx : x ∈ ↑f ⁻¹' Set.range ↑i
⊢ ↑f ↑{ val := x, property := hx } ∈ Set.range ↑i
Tactic:
simpa only [Set.mem_preimage]
Proof state after:
no goals
Theorem: CategoryTheory.aux_continuous_restrict
Proof state before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ Continuous (Set.restrict (↑f ⁻¹' Set.range ↑i) ↑f)
Tactic:
apply ContinuousOn.restrict
Proof state after:
case a
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ ContinuousOn (↑f) (↑f ⁻¹' Set.range ↑i)
Theorem: CategoryTheory.aux_continuous_restrict
Proof state before:
case a
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ ContinuousOn (↑f) (↑f ⁻¹' Set.range ↑i)
Tactic:
apply Continuous.continuousOn
Proof state after:
case a.h
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ Continuous ↑f
Theorem: CategoryTheory.aux_continuous_restrict
Proof state before:
case a.h
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ Continuous ↑f
Tactic:
exact f.continuous
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
⊢ lift f hi a b w ≫ snd f hi = b
Tactic:
dsimp [lift, snd, OpenEmbeddingCone, OpenEmbeddingConeRightMap, ContinuousMap.comp, Set.restrict, 
  Set.codRestrict, OpenEmbedding.InvRange]
Proof state after:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
⊢ (ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
      ContinuousMap.mk
        (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
          { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }) =
    b
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
⊢ (ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
      ContinuousMap.mk
        (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
          { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }) =
    b
Tactic:
ext z
Proof state after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Tactic:
have := congr_fun (FunLike.ext'_iff.mp w.symm) z
Proof state after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Tactic:
have h : i (b z) = f (a z) := this
Proof state after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Tactic:
suffices : b z = (Homeomorph.ofEmbedding i hi.toEmbedding).symm 
  (⟨f (a z), by rw [← h] ; simp⟩)
Proof state after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this✝ : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
this :
  ↑b z =
    ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)))
      { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z

case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑b z =
    ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)))
      { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑b z =
    ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)))
      { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
Tactic:
apply_fun (Homeomorph.ofEmbedding i hi.toEmbedding)
Proof state after:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑(Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)) (↑b z) =
    ↑(Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))
      (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)))
        { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) })
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑(Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)) (↑b z) =
    ↑(Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))
      (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)))
        { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) })
Tactic:
simp only [Homeomorph.apply_symm_apply]
Proof state after:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑(Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)) (↑b z) =
    { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑(Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)) (↑b z) =
    { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
Tactic:
dsimp [Homeomorph.ofEmbedding]
Proof state after:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ { val := ↑i (↑b z), property := (_ : ∃ y, ↑i y = ↑i (↑b z)) } =
    { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case this
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ { val := ↑i (↑b z), property := (_ : ∃ y, ↑i y = ↑i (↑b z)) } =
    { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
Tactic:
simp_rw [h]
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑f (↑a z) ∈ Set.range ↑i
Tactic:
rw [← h]
Proof state after:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑i (↑b z) ∈ Set.range ↑i
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
⊢ ↑i (↑b z) ∈ Set.range ↑i
Tactic:
simp
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd
Proof state before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a : W ⟶ X
b : W ⟶ Y
w : a ≫ f = b ≫ i
z : (forget ExtrDisc).obj W
this✝ : ↑(b ≫ i) z = ↑(a ≫ f) z
h : ↑i (↑b z) = ↑f (↑a z)
this :
  ↑b z =
    ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i)))
      { val := ↑f (↑a z), property := (_ : ↑f (↑a z) ∈ Set.range ↑i) }
⊢ ↑((ContinuousMap.mk fun z => { val := ↑a z, property := (_ : ↑a z ∈ ↑f ⁻¹' Set.range ↑i) }) ≫
          ContinuousMap.mk
            (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑i (_ : Embedding ↑i))) ∘ fun x =>
              { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ Set.range ↑i) }))
      z =
    ↑b z
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.pullback.hom_ext
Proof state before:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
hfst : a ≫ fst f hi = b ≫ fst f hi
⊢ a = b
Tactic:
ext z
Proof state after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
hfst : a ≫ fst f hi = b ≫ fst f hi
z : (forget ExtrDisc).obj W
⊢ ↑a z = ↑b z
Theorem: CategoryTheory.ExtrDisc.pullback.hom_ext
Proof state before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
hfst : a ≫ fst f hi = b ≫ fst f hi
z : (forget ExtrDisc).obj W
⊢ ↑a z = ↑b z
Tactic:
apply_fun (fun q => q z) at hfst
Proof state after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑a z = ↑b z
Theorem: CategoryTheory.ExtrDisc.pullback.hom_ext
Proof state before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑a z = ↑b z
Tactic:
apply Subtype.ext
Proof state after:
case w.a
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑(↑a z) = ↑(↑b z)
Theorem: CategoryTheory.ExtrDisc.pullback.hom_ext
Proof state before:
case w.a
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑(↑a z) = ↑(↑b z)
Tactic:
exact hfst
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.HasPullbackOpenEmbedding
Proof state before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ HasPullback f i
Tactic:
constructor
Proof state after:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ Nonempty (LimitCone (cospan f i))
Theorem: CategoryTheory.ExtrDisc.HasPullbackOpenEmbedding
Proof state before:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ Nonempty (LimitCone (cospan f i))
Tactic:
use OpenEmbeddingCone f hi
Proof state after:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ IsLimit (OpenEmbeddingCone f hi)
Theorem: CategoryTheory.ExtrDisc.HasPullbackOpenEmbedding
Proof state before:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ IsLimit (OpenEmbeddingCone f hi)
Tactic:
exact ExtrDisc.OpenEmbeddingLimitCone f hi
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.toExplicitCompFromExcplict
Proof state before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ toExplicit f hi ≫ fromExplicit f hi = 𝟙 (pullback f i)
Tactic:
refine' Limits.pullback.hom_ext (k := (toExplicit f hi ≫ fromExplicit f hi)) _ _
Proof state after:
case refine'_1
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.fst = 𝟙 (pullback f i) ≫ Limits.pullback.fst

case refine'_2
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.snd = 𝟙 (pullback f i) ≫ Limits.pullback.snd
Theorem: CategoryTheory.ExtrDisc.toExplicitCompFromExcplict
Proof state before:
case refine'_1
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.fst = 𝟙 (pullback f i) ≫ Limits.pullback.fst
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.toExplicitCompFromExcplict
Proof state before:
case refine'_2
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.snd = 𝟙 (pullback f i) ≫ Limits.pullback.snd
Tactic:
rw [Category.id_comp, Category.assoc, fromExplicit, Limits.pullback.lift_snd,
  toExplicit, pullback.lift_snd]
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.fromExcplictComptoExplicit
Proof state before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (fromExplicit f hi ≫ toExplicit f hi) ≫ pullback.fst f hi = 𝟙 (OpenEmbeddingCone f hi).pt ≫ pullback.fst f hi
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: CategoryTheory.ExtrDisc.compatibility
Proof state before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
⊢ δ hOpen f ≫ θ hOpen f ≫ η hOpen f = ζ hOpen f ≫ ε
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Theorem: CategoryTheory.ExtrDisc.compatibility
Proof state before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Tactic:
have := HasPullbackOpenEmbedding f (hOpen a)
Proof state after:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Theorem: CategoryTheory.ExtrDisc.compatibility
Proof state before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Tactic:
rw [← Category.assoc, δ, fromFiniteCoproduct, finiteCoproduct.ι_desc]
Proof state after:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ Sigma.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Theorem: CategoryTheory.ExtrDisc.compatibility
Proof state before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ Sigma.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Tactic:
simp [ε, ζ, θ, η, fromExplicit]
Proof state after:
no goals
Theorem: Profinite.toFiniteCoproductCompFromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
ext
Proof state after:
case h.w
α : Type
inst✝ : Fintype α
Z : α → Profinite
b✝ : α
x✝ : (forget Profinite).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Theorem: Profinite.toFiniteCoproductCompFromFiniteCoproduct
Proof state before:
case h.w
α : Type
inst✝ : Fintype α
Z : α → Profinite
b✝ : α
x✝ : (forget Profinite).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
Proof state after:
no goals