Theorem: Profinite.epi_pullback_of_epi (Profinite/ExplicitSheaves.lean)

State before:
⊢ EpiPullbackOfEpi Profinite
Tactic:
intro X Y Z f π hπ
State after:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi Limits.pullback.fst

State before:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi Limits.pullback.fst
Tactic:
suffices : Epi (fromExplicit f π ≫ (Limits.pullback.fst : Limits.pullback f π ⟶ Y))
State after:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
this : Epi (fromExplicit f π ≫ Limits.pullback.fst)
⊢ Epi Limits.pullback.fst

case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi (fromExplicit f π ≫ Limits.pullback.fst)

State before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi (fromExplicit f π ≫ Limits.pullback.fst)
Tactic:
rw [Profinite.epi_iff_surjective] at hπ ⊢
State after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
⊢ Function.Surjective ↑(fromExplicit f π ≫ Limits.pullback.fst)

State before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
⊢ Function.Surjective ↑(fromExplicit f π ≫ Limits.pullback.fst)
Tactic:
intro y
State after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y

State before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Tactic:
obtain ⟨z,hz⟩ := hπ (f y)
State after:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y

State before:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Tactic:
have : fromExplicit f π ≫ Limits.pullback.fst = Profinite.pullback.fst f π
State after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π

case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y

State before:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Tactic:
rw [this]
State after:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(pullback.fst f π) a = y

State before:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(pullback.fst f π) a = y
Tactic:
exact ⟨⟨(y, z), hz.symm⟩, rfl⟩
State after:
no goals

State before:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
this : Epi (fromExplicit f π ≫ Limits.pullback.fst)
⊢ Epi Limits.pullback.fst
Tactic:
exact @epi_of_epi _ _ _ _ _ _ _ this
State after:
no goals

State before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
Tactic:
dsimp [fromExplicit]
State after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ Limits.pullback.lift (pullback.fst f π) (pullback.snd f π) (_ : pullback.fst f π ≫ f = pullback.snd f π ≫ π) ≫
      Limits.pullback.fst =
    pullback.fst f π

State before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ Limits.pullback.lift (pullback.fst f π) (pullback.snd f π) (_ : pullback.fst f π ≫ f = pullback.snd f π ≫ π) ≫
      Limits.pullback.fst =
    pullback.fst f π
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
State after:
no goals