Theorem: CategoryTheory.vsurj (Sieves/ExtensiveRegular.lean)

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
α : Type
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
x✝ : (Y : C) × { f // S f }
Y : C
f : Y ⟶ X
hf : S f
⊢ ∃ a, v hS a = { fst := Y, snd := { val := f, property := hf } }
Tactic:
cases' (hS ▸ hf) with a h
State after:
case mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
α : Type
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
x✝ : (Y : C) × { f // S f }
a : α
hf : S (π a)
⊢ ∃ a_1, v hS a_1 = { fst := Z a, snd := { val := π a, property := hf } }

State before:
case mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
α : Type
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
x✝ : (Y : C) × { f // S f }
a : α
hf : S (π a)
⊢ ∃ a_1, v hS a_1 = { fst := Z a, snd := { val := π a, property := hf } }
Tactic:
exact ⟨a, rfl⟩
State after:
no goals