awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    (((ℱ.obj (P := Presheaf.IsSheaf K).mapIso e.op).toEquiv : (a : ℱ.obj.obj (op X)) → ℱ.obj.obj (op (F.obj X')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
              (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
            (x g₁ hg₁) :
          (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    (((ℱ.obj (P := Presheaf.IsSheaf K).mapIso e.op).toEquiv : (a : ℱ.obj.obj (op X)) → ℱ.obj.obj (op (F.obj X')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
              (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
            (x g₂ hg₂) :
          (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
have compatible : Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₁.op ≫ e.hom.op)) :
        (a : ℱ.obj.obj (op (F.obj Y₁))) → ℱ.obj.obj (op (F.obj X')))
      (x g₁ hg₁) :
    ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₂.op ≫ e.hom.op)) :
        (a : ℱ.obj.obj (op (F.obj Y₂))) → ℱ.obj.obj (op (F.obj X')))
      (x g₂ hg₂) :
    ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
Tactic: simp only [Iso.op_hom, Iso.toEquiv_fun, ℱ.1.mapIso_hom, ← Functor.map_comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
⊢ ∃! t : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X), x.IsAmalgamation (R := S.arrows) t
have hex : ∃ (x_1 : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
Tactic: apply existsUnique_of_exists_of_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
hex : ∃ (x_1 : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
⊢ ∃! t : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X), x.IsAmalgamation (R := S.arrows) t
have hunique : ∀ (y₁ y₂ : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)),
  x.IsAmalgamation (R := S.arrows) y₁ → x.IsAmalgamation (R := S.arrows) y₂ → y₁ = y₂
Tactic: apply existsUnique_of_exists_of_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
⊢ ∃ (x_1 : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
have H : IsSheafFor (G.obj (P := Presheaf.IsSheaf K)) (Sieve.functorPushforward F S).arrows
Tactic: have H := (isSheaf_iff_isSheaf_of_type _ _).1 G.2 _ (hF₂.cover_preserve hS)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
⊢ y₁ = y₂
have hunique : ∀ ⦃Y : D⦄ ⦃f : Y ⟶ F.obj X⦄,
  (Sieve.functorPushforward F S).arrows f →
    Eq (α := (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op (F.obj X)))) →
              (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op Y)))
          y₁ :
        (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op (F.obj X)))) →
              (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op Y)))
          y₂ :
        (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
Tactic: apply (((isSheaf_iff_isSheaf_of_type _ _).1 G.2).isSeparated _ (hF₂.cover_preserve hS)).ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
⊢ F.PreservesOneHypercovers J K
have refine_1 : ∀ {U : C} (E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U),
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U))
    (PreZeroHypercover.sieve₀.{w, v₂, u₂} (E.map F).toPreZeroHypercover)
Tactic: refine fun {U} E ↦ ⟨?_, fun i₁ i₂ W p₁ p₂ h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
refine_1 :
  ∀ {U : C} (E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U),
    Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U))
      (PreZeroHypercover.sieve₀.{w, v₂, u₂} (E.map F).toPreZeroHypercover)
⊢ F.PreservesOneHypercovers J K
have refine_2 : ∀ {U : C} (E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U) (i₁ i₂ : E.I₀) (W : D) (p₁ : W ⟶ F.obj (E.X i₁))
  (p₂ : W ⟶ F.obj (E.X i₂)) (h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)),
  (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W
Tactic: refine fun {U} E ↦ ⟨?_, fun i₁ i₂ W p₁ p₂ h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
⊢ (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W
have this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
Tactic: have : HasPullback ((E.toPreOneHypercover.map F).f i₁) ((E.toPreOneHypercover.map F).f i₂) :=
      hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W
have this₁ : Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
  ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
  (Sieve.functorPushforward F (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))))
Tactic: have := H.cover_preserve (E.mem₁ i₁ i₂ (pullback.fst (E.f i₁) (E.f i₂)) _ pullback.condition)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this_1 : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    (Sieve.functorPushforward F (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))))
⊢ (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W
have this₁ : Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
  ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
  ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
Tactic: rw [PreOneHypercover.functorPushforward_sieve₁_of_preservesPullbacks _ _ _
      pullback.condition] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverPreserving (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this_1 : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
⊢ (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W
have refine_2 : Sieve.pullback (X := F.obj (Limits.pullback (E.f i₁) (E.f i₂))) (IsPullback.lift sorry p₁ p₂ h)
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))) ≤
  (E.map F).sieve₁ p₁ p₂
Tactic: refine K.superset_covering ?_
      (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve.{v_1, u_1} Y
inst_1 : R.HasPullbacks f
Z : C
g : Z ⟶ X
⊢ Presieve.pullbackArrows f R g → ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ Y), R e ∧ i ≫ e = g ≫ f
have this : ∀ (W : C) (b : W ⟶ Y) (hb : R b), ∃ (W_1 : C) (i : pullback b f ⟶ W_1) (e : W_1 ⟶ Y), R e ∧ i ≫ e = pullback.snd b f ≫ f
Tactic: ⟨W, b, hb⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve.{v_1, u_1} Y
inst_1 : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
⊢ ∃ (W_1 : C) (i : pullback b f ⟶ W_1) (e : W_1 ⟶ Y), R e ∧ i ≫ e = pullback.snd b f ≫ f
have this : HasPullback b f
Tactic: have := R.hasPullback f hb
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
S : Presieve.{v_1, u_1} X
T : Sieve.{v_1, u_1} X
h : S.FactorsThru T.arrows
Y : C
f : Y ⟶ X
hf : S f
⊢ T.arrows f
have obtain : ∀ (W : C) (i : Y ⟶ W) (e : W ⟶ X) (h1 : T.arrows e) (hf : S (i ≫ e)), T.arrows (i ≫ e)
Tactic: obtain ⟨W, i, e, h1, rfl⟩ := h hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : S.FactorsThru T
hS : IsSheafFor P S
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
⊢ IsSheafFor P T
have simp : ∀
  (hS :
    IsSeparatedFor P S ∧
      ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t),
  IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
Tactic: simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : S.FactorsThru T
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
have choose : ∀ (W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C) (i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a)
  (e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X) (h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a))
  (h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g),
  IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
Tactic: choose W i e h1 h2 using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
have refine_1 : IsSeparatedFor P T
Tactic: refine ⟨?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
refine_1 : IsSeparatedFor P T
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
have refine_2 : ∀ (x : FamilyOfElements P T) (hx : x.Compatible (R := T)), ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
Tactic: refine ⟨?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation (R := T) y₁
h₂ : x.IsAmalgamation (R := T) y₂
⊢ y₁ = y₂
have refine_1 : ∀ (Y : C) (g : Y ⟶ X) (hg : S g),
  Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
        y₁ :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
        y₂ :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
Tactic: refine hS.1.ext (fun Y g hg => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y₁))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (y f₁ h₁) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y₂))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (y f₂ h₂) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
have rw : Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₁ ≫ i h₁).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₁)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
      (x (e h₁) sorry) :
    (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₂ ≫ i h₂).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₂)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
      (x (e h₂) sorry) :
    (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
Tactic: rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op),
      ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op),
      ← P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₁ ≫ i h₁).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₁)))) →
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (x (e h₁) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₂ ≫ i h₂).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₂)))) →
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (x (e h₂) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
have a : (g₁ ≫ i h₁) ≫ e h₁ = (g₂ ≫ i h₂) ≫ e h₂
Tactic: apply hx