awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (hypothesis)
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₂))) ⋯)
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
have 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₂))
Tactic: simp only [pullback.hom_ext_iff, Category.assoc, limit.lift_π, PullbackCone.mk_π_app] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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 = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
have 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) sorry))
    (F.map (pullback.fst (E.f i₁) (E.f i₂)))
Tactic: apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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₂)))
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
have 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) sorry))
    (F.map (pullback.snd (E.f i₁) (E.f i₂)))
Tactic: apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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₂)
have refine : (E.map F).sieve₁ (F.map p₁) (F.map p₂) ≤ Sieve.functorPushforward F (E.sieve₁ p₁ p₂)
Tactic: refine le_antisymm (PreOneHypercover.functorPushforward_sieve₁_map_le _ _ _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (hypothesis)
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
⊢ (E.map F).sieve₁ (F.map p₁) (F.map p₂) ≤ Sieve.functorPushforward F (E.sieve₁ p₁ p₂)
have this : 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₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (hypothesis)
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
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
have hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
Tactic: have hl₁ : l ≫ pullback.fst _ _ = p₁ := by simp [l]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (hypothesis)
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₁
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
have hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
Tactic: have hl₂ : l ≫ pullback.snd _ _ = p₂ := by simp [l]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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
have refine_1 : f ≫ F.map l = u ≫ F.map r
Tactic: refine ⟨pullback l r, pullback.fst _ _, IsPullback.lift
    (IsPullback.map _ (.of_hasPullback _ _)) f u ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
have refine_2 : (E.sieve₁ p₁ p₂).arrows (Y := pullback l r) (pullback.fst l r)
Tactic: refine ⟨pullback l r, pullback.fst _ _, IsPullback.lift
    (IsPullback.map _ (.of_hasPullback _ _)) f u ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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)
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
have refine_3 : f = CategoryStruct.comp (Y := F.obj (pullback l r)) (IsPullback.lift sorry f u sorry) (F.map (pullback.fst l r))
Tactic: refine ⟨pullback l r, pullback.fst _ _, IsPullback.lift
    (IsPullback.map _ (.of_hasPullback _ _)) f u ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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 = u ≫ F.map r
have 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₂))
Tactic: apply (IsPullback.map _ (.of_hasPullback _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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₂))
⊢ f ≫ F.map l = u ≫ F.map r
have 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₂))
Tactic: apply (IsPullback.map _ (.of_hasPullback _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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)
have refine_2 : Eq (α := pullback l r ⟶ E.X i₁) (pullback.fst l r ≫ p₁) (pullback.snd l r ≫ E.p₁ k)
Tactic: refine ⟨k, pullback.snd _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
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_2 : Eq (α := pullback l r ⟶ E.X i₁) (pullback.fst l r ≫ p₁) (pullback.snd l r ≫ E.p₁ k)
⊢ (E.sieve₁ p₁ p₂).arrows (Y := pullback l r) (pullback.fst l r)
have refine_2₁ : Eq (α := pullback l r ⟶ E.X i₂) (pullback.fst l r ≫ p₂) (pullback.snd l r ≫ E.p₂ k)
Tactic: refine ⟨k, pullback.snd _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Function.Bijective (β := H.obj G ⟶ U) fun (g : H.obj G' ⟶ U) ↦ H.map f ≫ g
have rw : Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
  fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U) ↦ f ≫ g
Tactic: rw [adj.map_comp_bijective_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
    fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U) ↦ f ≫ g
have a : Presheaf.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Presheaf.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
have a : Presieve.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))) F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf J (F.op ⋙ G)
have refine : ∀ ⦃X : C⦄ ⦃S : Sieve.{v₁, u₁} X⦄,
  S ∈ (J : (a : C) → Set (Sieve a)) X →
    K.W (X :=
      H'.obj
        (Subfunctor.toFunctor (F := obj shrinkYoneda.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} X)
          (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
      (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
Tactic: refine Presieve.IsSheaf.comp_of_W_map_of_adjunction _ adj' ?_ _ hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))) F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ K.W (X :=
    H'.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
    (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
have hWS : J.W (X :=
  Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
    (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
  (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
Tactic: have hWS : J.W (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂} S).ι :=
    Sieve.W_shrinkFunctor_ι_of_mem.{max u₁ v₁ u₂ v₂} _ S hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))) F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
hWS :
  J.W (X :=
    Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
      (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
    (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
⊢ K.W (X :=
    H'.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
    (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
have this : K.W (X :=
  H.obj
    (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
      (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
  (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
Tactic: have : K.W _ := Functor.W_map_of_adjunction_of_isContinuous_aux (J := J) K F H adj
    (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂} S).ι hWS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))) F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
hWS :
  J.W (X :=
    Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
      (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
    (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
this :
  K.W (X :=
    H.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
    (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
e : H ⋙
    obj (whiskeringRight Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ≅
  obj (whiskeringRight Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ⋙
    H' :=
  uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}.lanCompIsoOfPreserves F.op
iso : Arrow.mk (X :=
    H'.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max w u₁ v₁ u₂ v₂, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S)))
    (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S))) ≅
  Arrow.mk (X :=
    H.obj
        (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
          (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)) ⋙
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
    (whiskerRight (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ K.W (X :=
    H'.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
    (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
have rw : K.W (X :=
  H.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)) ⋙
    uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
  (whiskerRight (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
    uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
Tactic: rw [K.W.arrow_mk_iso_iff iso]