internlm/Lean-Github huggingface dataset:
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
let F₂ : (Over.mk (g₂ ≫ f₂) : Over X) ⟶ (Over.mk f₂ : Over X) := (Over.homMk g₂)
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
have hF := @this ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ F
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
have hF₁ := @this ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk f₁, hf₁⟩ F₁
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
hF₁ :
  (diagram S.arrows).map F₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₁
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
hF₁ :
  (diagram S.arrows).map F₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₁
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
have hF₂ := @this ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ ⟨Over.mk f₂, hf₂⟩ F₂
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
hF₁ :
  (diagram S.arrows).map F₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₁
hF₂ :
  (diagram S.arrows).map F₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ } =
    s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₂
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
hF₁ :
  (diagram S.arrows).map F₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₁
hF₂ :
  (diagram S.arrows).map F₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ } =
    s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₂
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
simp at this ⊢
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
hF₁ :
  (diagram S.arrows).map F₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₁
hF₂ :
  (diagram S.arrows).map F₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ } =
    s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₂
this : ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y), f.left ≫ s.ι.app Y = s.ι.app X_1
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z)
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂
hF :
  (diagram S.arrows).map F ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F
hF₁ :
  (diagram S.arrows).map F₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₁
hF₂ :
  (diagram S.arrows).map F₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ } =
    s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } ≫
      ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map F₂
this : ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y), f.left ≫ s.ι.app Y = s.ι.app X_1
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Tactic:
aesop_cat
Proof state after:
no goals
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
⊢ S.arrows (g₁ ≫ f₁)
Tactic:
exact Sieve.downward_closed S hf₁ g₁
Proof state after:
no goals
Theorem: Sieve.yonedaFamily_fromCocone_compatible
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
s : Cocone (diagram S.arrows)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
this :
  ∀ ⦃X_1 Y : FullSubcategory fun f => S.arrows f.hom⦄ (f : X_1 ⟶ Y),
    (diagram S.arrows).map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ ((Functor.const (FullSubcategory fun f => S.arrows f.hom)).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
⊢ S.arrows (g₂ ≫ f₂)
Tactic:
exact Sieve.downward_closed S hf₂ g₂
Proof state after:
no goals
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) ↔ Nonempty (IsColimit (cocone S.arrows))
Tactic:
constructor
Proof state after:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit (cocone S.arrows))

case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ Nonempty (IsColimit (cocone S.arrows)) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit (cocone S.arrows))
Tactic:
intro H
Proof state after:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit (cocone S.arrows))
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit (cocone S.arrows))
Tactic:
refine Nonempty.intro ?mp.val
Proof state after:
case mp.val
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit (cocone S.arrows)
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
case mp.val
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit (cocone S.arrows)
Tactic:
exact {
desc := fun s => H s.pt (yonedaFamilyOfElements_fromCocone S s)
    (yonedaFamily_fromCocone_compatible S s) |>.choose
fac := by
  intro s f
  replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
     (yonedaFamily_fromCocone_compatible S s)
  have ht := H.choose_spec.1 f.obj.hom f.property
  aesop_cat
uniq := by
  intro s Fs HFs
  replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
      (yonedaFamily_fromCocone_compatible S s)
  apply H.choose_spec.2 Fs
  exact fun _ f hf => HFs ⟨Over.mk f, hf⟩
}
Proof state after:
no goals
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone (diagram S.arrows)) (j : FullSubcategory fun f => S.arrows f.hom),
    (cocone S.arrows).ι.app j ≫
        (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t))
          s =
      s.ι.app j
Tactic:
intro s f
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
   (yonedaFamily_fromCocone_compatible S s)
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Tactic:
have ht := H.choose_spec.1 f.obj.hom f.property
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
ht :
  (yoneda.obj s.pt).map f.obj.hom.op (Exists.choose H) =
    yonedaFamilyOfElements_fromCocone S s f.obj.hom (_ : S.arrows f.obj.hom)
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
f : FullSubcategory fun f => S.arrows f.hom
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
ht :
  (yoneda.obj s.pt).map f.obj.hom.op (Exists.choose H) =
    yonedaFamilyOfElements_fromCocone S s f.obj.hom (_ : S.arrows f.obj.hom)
⊢ (cocone S.arrows).ι.app f ≫
      (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s =
    s.ι.app f
Tactic:
aesop_cat
Proof state after:
no goals
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone (diagram S.arrows)) (m : (cocone S.arrows).pt ⟶ s.pt),
    (∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ m = s.ι.app j) →
      m =
        (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Tactic:
intro s Fs HFs
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S s)
    (yonedaFamily_fromCocone_compatible S s)
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ Fs = (fun s => Exists.choose (_ : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t)) s
Tactic:
apply H.choose_spec.2 Fs
Proof state after:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) Fs
Theorem: Sieve.Yoneda_sheaf_iff_colimit
Proof state before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone (diagram S.arrows)
Fs : (cocone S.arrows).pt ⟶ s.pt
HFs : ∀ (j : FullSubcategory fun f => S.arrows f.hom), (cocone S.arrows).ι.app j ≫ Fs = s.ι.app j
H : ∃! t, FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) t
⊢ FamilyOfElements.IsAmalgamation (yonedaFamilyOfElements_fromCocone S s) Fs
Tactic:
exact fun _ f hf => HFs ⟨Over.mk f, hf⟩
Proof state after:
no goals