internlm/Lean-Github huggingface dataset:
Theorem: EffectiveEpiFamily_transitive
Proof 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]
Proof 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))))
Theorem: EffectiveEpiFamily_transitive
Proof 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'
Proof 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₁
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof 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)
Theorem: EffectiveEpiFamily_transitive
Proof 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⟩
Proof 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)
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof 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)
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof 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)
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof state after:
no goals
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof 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)
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof 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
Theorem: EffectiveEpiFamily_transitive
Proof 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
Proof 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
Theorem: EffectiveEpiFamily_transitive
Proof 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)⟩
Proof state after:
no goals
Theorem: EffectiveEpiFamily_transitive
Proof 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)
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
constructor
Proof state after:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X

case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X → ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
exact coherentTopology.Sieve_of_has_EffectiveEpiFamily X S
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X → ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
intro h
Proof state after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
induction' h with Y T hS  Y Y R S _ _ a b
Proof state after:
case mpr.of
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ Coverage.covering (coherentCoverage C) Y
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

case mpr.top
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), ⊤.arrows (π a)

case mpr.transitive
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
a : ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.of
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ Coverage.covering (coherentCoverage C) Y
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Tactic:
rcases hS with ⟨a, h, Y', π, h'⟩
Proof state after:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Tactic:
use a, h, Y', π
Proof state after:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ EffectiveEpiFamily Y' π ∧ ∀ (a : a), (Sieve.generate T).arrows (π a)