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

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
⊢ isPullbackPresieve S
Tactic:
rcases hS with ⟨α, _, Z, π, hS, HIso⟩
State after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ isPullbackPresieve S

State before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ isPullbackPresieve S
Tactic:
intro Y₁ Y₂ f hf g hg
State after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : S f
g : Y₂ ⟶ X
hg : S g
⊢ HasPullback f g

State before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : S f
g : Y₂ ⟶ X
hg : S g
⊢ HasPullback f g
Tactic:
rw [hS] at hf hg
State after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
g : Y₂ ⟶ X
hg : Presieve.ofArrows Z π g
⊢ HasPullback f g

State before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
g : Y₂ ⟶ X
hg : Presieve.ofArrows Z π g
⊢ HasPullback f g
Tactic:
cases' hg with b
State after:
case intro.intro.intro.intro.intro.mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
b : α
⊢ HasPullback f (π b)

State before:
case intro.intro.intro.intro.intro.mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
b : α
⊢ HasPullback f (π b)
Tactic:
apply HasPullbackOfIsIsodesc.HasPullback f
State after:
no goals