awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
refine_1 :
  LE.le (α := Sieve.{v₂, u₂} (F.obj (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₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
⊢ LE.le (α := Sieve.{v₂, u₂} (F.obj (pullback (E.f i₁) (E.f i₂)))) (Sieve.functorPushforward F (E.sieve₁' i₁ 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.sieve₁'_eq_sieve₁]

Premises used: CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ LE.le (α := Sieve.{v₂, u₂} (F.obj (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₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))

Tactic:
apply PreOneHypercover.functorPushforward_sieve₁_map_le

Premises used: CategoryTheory.PreOneHypercover.functorPushforward_sieve₁_map_le
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Eq (α := F.obj (pullback (E.f i₁) (E.f i₂)) ⟶ F.obj X) (F.map (pullback.fst (E.f i₁) (E.f i₂)) ≫ (E.map F).f i₁)
    (F.map (pullback.snd (E.f i₁) (E.f i₂)) ≫ (E.map F).f i₂)

Tactic:
simp [← Functor.map_comp, pullback.condition]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
refine_2 :
  LE.le (α := Sieve.{v₂, u₂} (F.obj (pullback (E.f i₁) (E.f i₂))))
    (Sieve.pullback (X := pullback ((E.map F).f i₁) ((E.map F).f i₂))
      (pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
      ((E.map F).sieve₁' i₁ i₂))
    (Sieve.functorPushforward F (E.sieve₁' i₁ i₂))
⊢ LE.le (α := Sieve.{v₂, u₂} (F.obj (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₂))))
    (Sieve.functorPushforward F (E.sieve₁' i₁ i₂))

Tactic:
rw [PreOneHypercover.sieve₁_eq_pullback_sieve₁' _ _ _
      (by simp [← Functor.map_comp, pullback.condition])]

Premises used: CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁'
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  Eq (α := W ⟶ pullback ((E.map F).f i₁) ((E.map F).f i₂)) (u ≫ (E.map F).toPullback k)
    (f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
⊢ Sieve.arrows (Sieve.functorPushforward F (E.sieve₁' i₁ i₂)) f

Tactic:
⟨E.Y k, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), u, ?_, ?_⟩

Premises used: CategoryTheory.Limits.pullback.lift, CategoryTheory.PreOneHypercover.Y, CategoryTheory.PreOneHypercover.w, And.intro, CategoryTheory.PreOneHypercover.p₂, Exists.intro, CategoryTheory.Presieve.functorPushforward, CategoryTheory.PreOneHypercover.p₁
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  Eq (α := W ⟶ pullback ((E.map F).f i₁) ((E.map F).f i₂)) (u ≫ (E.map F).toPullback k)
    (f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
refine_2 : Sieve.arrows (X := pullback (E.f i₁) (E.f i₂)) (E.sieve₁' i₁ i₂) (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
refine_2₁ : f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
⊢ Sieve.arrows (Sieve.functorPushforward F (E.sieve₁' i₁ i₂)) f

Tactic:
refine ⟨E.Y k, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), u, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  Eq (α := W ⟶ pullback ((E.map F).f i₁) ((E.map F).f i₂)) (u ≫ (E.map F).toPullback k)
    (f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
right :
  Eq (α := E.Y k ⟶ pullback (E.f i₁) (E.f i₂)) (𝟙 (E.Y k) ≫ pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
    (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
⊢ Sieve.arrows (X := pullback (E.f i₁) (E.f i₂)) (E.sieve₁' i₁ i₂) (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
use E.Y k, 𝟙 _, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), ⟨k⟩

Premises used: CategoryTheory.Limits.pullback.lift, CategoryTheory.CategoryStruct.id, CategoryTheory.PreOneHypercover.Y, CategoryTheory.PreOneHypercover.w, CategoryTheory.PreOneHypercover.p₂, CategoryTheory.PreOneHypercover.p₁
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  Eq (α := W ⟶ pullback ((E.map F).f i₁) ((E.map F).f i₂)) (u ≫ (E.map F).toPullback k)
    (f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
⊢ Eq (α := E.Y k ⟶ pullback (E.f i₁) (E.f i₂)) (𝟙 (E.Y k) ≫ pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
    (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  Eq (α := W ⟶ pullback ((E.map F).f i₁) ((E.map F).f i₂)) (u ≫ (E.map F).toPullback k)
    (f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
⊢ u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))

Tactic:
simp only [pullback.hom_ext_iff, Category.assoc, limit.lift_π, PullbackCone.mk_π_app] at h

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.pullback.hom_ext_iff, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
refine_2 :
  f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) =
    CategoryStruct.comp (Y := F.obj (pullback (E.f i₁) (E.f i₂))) (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯))
      (F.map (pullback.fst (E.f i₁) (E.f i₂)))
refine_2₁ :
  f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) =
    CategoryStruct.comp (Y := F.obj (pullback (E.f i₁) (E.f i₂))) (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯))
      (F.map (pullback.snd (E.f i₁) (E.f i₂)))
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _))

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) =
    CategoryStruct.comp (Y := F.obj (pullback (E.f i₁) (E.f i₂))) (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯))
      (F.map (pullback.fst (E.f i₁) (E.f i₂)))

Tactic:
simp [← h.left, ← h.right, ← Functor.map_comp]

Premises used: And.right, And.left, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) =
    CategoryStruct.comp (Y := F.obj (pullback (E.f i₁) (E.f i₂))) (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯))
      (F.map (pullback.snd (E.f i₁) (E.f i₂)))

Tactic:
simp [← h.left, ← h.right, ← Functor.map_comp]

Premises used: And.right, And.left, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) = (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
le_antisymm (PreOneHypercover.functorPushforward_sieve₁_map_le _ _ _) ?_

Premises used: le_antisymm, CategoryTheory.PreOneHypercover.functorPushforward_sieve₁_map_le
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
refine : (E.map F).sieve₁ (F.map p₁) (F.map p₂) ≤ Sieve.functorPushforward F (E.sieve₁ p₁ p₂)
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) = (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
refine le_antisymm (PreOneHypercover.functorPushforward_sieve₁_map_le _ _ _) ?_

Premises used: le_antisymm, CategoryTheory.PreOneHypercover.functorPushforward_sieve₁_map_le
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
⊢ HasPullback ((E.map F).f i₁) ((E.map F).f i₂)

Tactic:
have : HasPullback ((E.map F).f i₁) ((E.map F).f i₂) :=
    hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
⊢ l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁

Tactic:
simp [l]
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
⊢ l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁

Tactic:
have hl₁ : l ≫ pullback.fst _ _ = p₁ := by simp [l]
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
⊢ l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂

Tactic:
simp [l]
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
⊢ l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂

Tactic:
have hl₂ : l ≫ pullback.snd _ _ = p₂ := by simp [l]
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f

Tactic:
⟨pullback l r, pullback.fst _ _, IsPullback.lift
    (IsPullback.map _ (.of_hasPullback _ _)) f u ?_, ?_, ?_⟩

Premises used: CategoryTheory.Limits.pullback, And.intro, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.map, CategoryTheory.IsPullback.lift, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
refine_1 : f ≫ F.map l = u ≫ F.map r
refine_2 : (E.sieve₁ p₁ p₂).arrows (Y := pullback l r) (pullback.fst l r)
refine_3 : f = CategoryStruct.comp (Y := F.obj (pullback l r)) (IsPullback.lift ⋯ f u ⋯) (F.map (pullback.fst l r))
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f

Tactic:
refine ⟨pullback l r, pullback.fst _ _, IsPullback.lift
    (IsPullback.map _ (.of_hasPullback _ _)) f u ?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
refine_1 :
  (f ≫ F.map l) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) = (u ≫ F.map r) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂))
refine_1₁ :
  (f ≫ F.map l) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) = (u ≫ F.map r) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map l = u ≫ F.map r

Tactic:
apply (IsPullback.map _ (.of_hasPullback _ _)).hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ (f ≫ F.map l) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) = (u ≫ F.map r) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂))

Tactic:
simp [l, r, ← Functor.map_comp, hf₁, hf₂]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ (f ≫ F.map l) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) = (u ≫ F.map r) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))

Tactic:
simp [l, r, ← Functor.map_comp, hf₁, hf₂]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ (E.sieve₁ p₁ p₂).arrows (Y := pullback l r) (pullback.fst l r)

Tactic:
⟨k, pullback.snd _ _, ?_, ?_⟩

Premises used: CategoryTheory.Limits.pullback.snd, And.intro, Exists.intro