Theorem: CategoryTheory.ExtrDisc.pullback.lift_snd (ExtrDisc/Pullback.lean)

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]
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

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
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

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
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

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
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

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⟩)
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) }

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)
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) })

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]
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) }

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]
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) }

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]
State after:
no goals

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]
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

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
State after:
no goals

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
State after:
no goals