Theorem: EffectiveEpiFamily_transitive (ExtrDisc/Topologies.lean)

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst
Tactic:
rw [← Sieve.effectiveEpimorphic_family]
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpimorphic (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ EffectiveEpimorphic (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
Tactic:
suffices h₂ : (Sieve.generate (Presieve.ofArrows (fun (⟨a, b⟩ : Σ _, β _) => Y_n a b)
      (fun ⟨a,b⟩ => π_n a b ≫ π a))) ∈ GrothendieckTopology.sieves (coherentTopology C) X by
  change Nonempty _
  rw [← Sieve.Yoneda_sheaf_iff_colimit]
  intro W
  apply coherentTopology.isSheaf_Yoneda
  exact h₂
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
let h' := h
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpiFamily Y π := h
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpiFamily Y π := h
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
rw [← Sieve.effectiveEpimorphic_family] at h'
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
let H' := H
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) := H
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
conv at H' =>
  intro a
  rw [← Sieve.effectiveEpimorphic_family]
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
apply Coverage.saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
State after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Coverage.saturate (coherentCoverage C) X (Sieve.generate (ofArrows Y π))

case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (ofArrows Y π)).arrows f →
      Coverage.saturate (coherentCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a)))

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ EffectiveEpimorphic (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)
Tactic:
change Nonempty _
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ Nonempty
    (IsColimit
      (cocone (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows))

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ Nonempty
    (IsColimit
      (cocone (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows))
Tactic:
rw [← Sieve.Yoneda_sheaf_iff_colimit]
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∀ (W : C),
    IsSheafFor (yoneda.obj W)
      (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∀ (W : C),
    IsSheafFor (yoneda.obj W)
      (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
Tactic:
intro W
State after:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ IsSheafFor (yoneda.obj W)
    (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows

State before:
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ IsSheafFor (yoneda.obj W)
    (Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows
Tactic:
apply coherentTopology.isSheaf_Yoneda
State after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst) ∈
    GrothendieckTopology.sieves (coherentTopology C) X

State before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (ofArrows
        (fun x =>
          match x with
          | { fst := a, snd := b } => Y_n a b)
        fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
W : C
⊢ Sieve.generate (ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst) ∈
    GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
exact h₂
State after:
no goals

State before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ Coverage.saturate (coherentCoverage C) X (Sieve.generate (ofArrows Y π))
Tactic:
apply Coverage.saturate.of
State after:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π ∈ Coverage.covering (coherentCoverage C) X

State before:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π ∈ Coverage.covering (coherentCoverage C) X
Tactic:
use α, inferInstance, Y, π
State after:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π = ofArrows Y π ∧ EffectiveEpiFamily Y π

State before:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ofArrows Y π = ofArrows Y π ∧ EffectiveEpiFamily Y π
Tactic:
simp only [true_and]
State after:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ EffectiveEpiFamily Y π

State before:
case a.hS
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ EffectiveEpiFamily Y π
Tactic:
exact Iff.mp (Sieve.effectiveEpimorphic_family Y π) h'
State after:
no goals

State before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (ofArrows Y π)).arrows f →
      Coverage.saturate (coherentCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a)))
Tactic:
intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
State after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)))

State before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)))
Tactic:
rw [← hf, Sieve.pullback_comp]
State after:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (ofArrows
            (fun x =>
              match x with
              | { fst := a, snd := b } => Y_n a b)
            fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a))))

State before:
case a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Coverage.saturate (coherentCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (ofArrows
            (fun x =>
              match x with
              | { fst := a, snd := b } => Y_n a b)
            fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a))))
Tactic:
apply (coherentTopology C).pullback_stable'
State after:
case a.a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Sieve.pullback g
      (Sieve.generate
        (ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)) ∈
    GrothendieckTopology.sieves (coherentTopology C) Y₁

State before:
case a.a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ Sieve.pullback g
      (Sieve.generate
        (ofArrows
          (fun x =>
            match x with
            | { fst := a, snd := b } => Y_n a b)
          fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)) ∈
    GrothendieckTopology.sieves (coherentTopology C) Y₁
Tactic:
apply coherentTopology.Sieve_of_has_EffectiveEpiFamily
State after:
case a.a.a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ ∃ α_1 x Y_1 π_1,
    EffectiveEpiFamily Y_1 π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback g
              (Sieve.generate
                (ofArrows
                  (fun x =>
                    match x with
                    | { fst := a, snd := b } => Y_n a b)
                  fun x =>
                  match x with
                  | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
          (π_1 a)

State before:
case a.a.a
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : ofArrows Y π g
hf : h ≫ g = f
⊢ ∃ α_1 x Y_1 π_1,
    EffectiveEpiFamily Y_1 π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback g
              (Sieve.generate
                (ofArrows
                  (fun x =>
                    match x with
                    | { fst := a, snd := b } => Y_n a b)
                  fun x =>
                  match x with
                  | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
          (π_1 a)
Tactic:
rcases hY with ⟨i⟩
State after:
case a.a.a.mk
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∃ α_1 x Y π_1,
    EffectiveEpiFamily Y π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback (π i)
              (Sieve.generate
                (ofArrows
                  (fun x =>
                    match x with
                    | { fst := a, snd := b } => Y_n a b)
                  fun x =>
                  match x with
                  | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
          (π_1 a)

State before:
case a.a.a.mk
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∃ α_1 x Y π_1,
    EffectiveEpiFamily Y π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback (π i)
              (Sieve.generate
                (ofArrows
                  (fun x =>
                    match x with
                    | { fst := a, snd := b } => Y_n a b)
                  fun x =>
                  match x with
                  | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
          (π_1 a)
Tactic:
use β i, inferInstance, Y_n i, π_n i
State after:
case a.a.a.mk
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ EffectiveEpiFamily (Y_n i) (π_n i) ∧
    ∀ (a : β i),
      (Sieve.pullback (π i)
            (Sieve.generate
              (ofArrows
                (fun x =>
                  match x with
                  | { fst := a, snd := b } => Y_n a b)
                fun x =>
                match x with
                | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
        (π_n i a)

State before:
case a.a.a.mk
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ EffectiveEpiFamily (Y_n i) (π_n i) ∧
    ∀ (a : β i),
      (Sieve.pullback (π i)
            (Sieve.generate
              (ofArrows
                (fun x =>
                  match x with
                  | { fst := a, snd := b } => Y_n a b)
                fun x =>
                match x with
                | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
        (π_n i a)
Tactic:
constructor
State after:
case a.a.a.mk.left
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ EffectiveEpiFamily (Y_n i) (π_n i)

case a.a.a.mk.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∀ (a : β i),
    (Sieve.pullback (π i)
          (Sieve.generate
            (ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
      (π_n i a)

State before:
case a.a.a.mk.left
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ EffectiveEpiFamily (Y_n i) (π_n i)
Tactic:
exact H i
State after:
no goals

State before:
case a.a.a.mk.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∀ (a : β i),
    (Sieve.pullback (π i)
          (Sieve.generate
            (ofArrows
              (fun x =>
                match x with
                | { fst := a, snd := b } => Y_n a b)
              fun x =>
              match x with
              | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
      (π_n i a)
Tactic:
intro b
State after:
case a.a.a.mk.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ (Sieve.pullback (π i)
        (Sieve.generate
          (ofArrows
            (fun x =>
              match x with
              | { fst := a, snd := b } => Y_n a b)
            fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
    (π_n i b)

State before:
case a.a.a.mk.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ (Sieve.pullback (π i)
        (Sieve.generate
          (ofArrows
            (fun x =>
              match x with
              | { fst := a, snd := b } => Y_n a b)
            fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a))).arrows
    (π_n i b)
Tactic:
use Y_n i b, (𝟙 _), π_n i b ≫ π i
State after:
case a.a.a.mk.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ ofArrows
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      (fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a)
      (π_n i b ≫ π i) ∧
    𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i

State before:
case a.a.a.mk.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ ofArrows
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      (fun x =>
        match x with
        | { fst := a, snd := b } => π_n a b ≫ π a)
      (π_n i b ≫ π i) ∧
    𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i
Tactic:
constructor
State after:
case a.a.a.mk.right.left
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ ofArrows
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    (fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a)
    (π_n i b ≫ π i)

case a.a.a.mk.right.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ 𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i

State before:
case a.a.a.mk.right.left
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ ofArrows
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    (fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a)
    (π_n i b ≫ π i)
Tactic:
exact ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩
State after:
no goals

State before:
case a.a.a.mk.right.right
C : Type u
inst✝³ : Category C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Fintype α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : (a : α) → Fintype (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y✝ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h' : EffectiveEpimorphic (ofArrows Y✝ π)
H' : ∀ (a : α), EffectiveEpimorphic (ofArrows (Y_n a) (π_n a))
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
b : β i
⊢ 𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i
Tactic:
exact Category.id_comp (π_n i b ≫ π i)
State after:
no goals