awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Eq (α := CA ((H.op ⋙ G).obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op Z)) :
          (a : CA ((H.op ⋙ F).obj (Opposite.op Z))) → CA ((H.op ⋙ G).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
            a :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA ((H.op ⋙ G).obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op Z)) :
          (a : CA ((H.op ⋙ F).obj (Opposite.op Z))) → CA ((H.op ⋙ G).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
            b :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA ((H.op ⋙ G).obj (Opposite.op Z)))
have h₁ : Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
        (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
            (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
          a :
        CA (F.obj (Opposite.op (H.obj Z)))) :
    CA (G.obj (Opposite.op (H.obj Z))))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
        (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
            (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
          b :
        CA (F.obj (Opposite.op (H.obj Z)))) :
    CA (G.obj (Opposite.op (H.obj Z))))
Tactic: simp only [comp_obj, op_obj, whiskerLeft_app, Opposite.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            a :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            b :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
have h₁ : Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) : (a : CA (G.obj X)) → CA (G.obj (Opposite.op (H.obj Z))))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X)) :
    CA (G.obj (Opposite.op (H.obj Z))))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
        (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
            (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
          b :
        CA (F.obj (Opposite.op (H.obj Z)))) :
    CA (G.obj (Opposite.op (H.obj Z))))
Tactic: rw [NatTrans.naturality_apply, NatTrans.naturality_apply, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
⊢ imageSieve (FA := FA) (CA := CA) f a ∈ (K : (a : D) → Set (Sieve a)) X
have h : ∀ ⦃Y : D⦄ ⦃f_1 : Y ⟶ X⦄,
  (Sieve.coverByImage H X).arrows f_1 →
    Sieve.pullback f_1 (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: apply K.transitive (H.is_cover_of_isCoverDense K X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
⊢ (Sieve.coverByImage H X).arrows g →
    Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y
have h : ∀ (Z : C) (lift : Y ⟶ H.obj Z) (m : H.obj Z ⟶ X) (fac : lift ≫ m = g),
  Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: ⟨⟨Z, lift, m, fac⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y
have h : Sieve.pullback lift (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a)) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: rw [← fac, Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Sieve.pullback lift (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a)) ∈ (K : (a : D) → Set (Sieve a)) Y
have h : Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
  (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))
Tactic: apply K.pullback_stable
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))
have hh : Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
  ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
  (Sieve.functorPushforward H
    (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
          (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
        a)))
Tactic: have hh := hH.cover_preserve <| imageSieve_mem J (whiskerLeft H.op f) (G.map m.op a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
    ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
    (Sieve.functorPushforward H
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a)))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))
have h : Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
  (Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))))
Tactic: refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
    ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
    (Sieve.functorPushforward H
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a)))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))))
have h : imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
        (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
      a) ≤
  Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))
Tactic: refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_) hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
    ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
    (Sieve.functorPushforward H
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a)))
W : C
q : W ⟶ Z
⊢ Sieve.arrows
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a))
      q →
    (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))).arrows q
have h : ∀ (x : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) ((H.op ⋙ F).obj (Opposite.op W)))
  (h :
    Eq (α := CA ((H.op ⋙ G).obj (Opposite.op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op W)) :
            (a : CA ((H.op ⋙ F).obj (Opposite.op W))) → CA ((H.op ⋙ G).obj (Opposite.op W)))
          x :
        CA ((H.op ⋙ G).obj (Opposite.op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op ⋙ G).map q.op) :
            (a : CA ((H.op ⋙ G).obj (Opposite.op (Opposite.unop (Opposite.op Z))))) →
              CA ((H.op ⋙ G).obj (Opposite.op W)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
                (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
              a :
            CA (G.obj (Opposite.op (H.obj Z)))) :
        CA ((H.op ⋙ G).obj (Opposite.op W)))),
  (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))).arrows q
Tactic: ⟨x, h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : J.PreservesSheafification F
inst_4 : HasWeakSheafify.{v, v_2, u, u_2} J B
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso (X := obj (presheafToSheaf J B) (P₁ ⋙ F)) (map (presheafToSheaf J B) (whiskerRight f F))
have rw : J.W (whiskerRight f F)
Tactic: rw [← W_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_4 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_5 : J.PreservesSheafification F
⊢ IsIso (X := obj (whiskeringRight Cᵒᵖ A B) F ⋙ presheafToSheaf J B) (Y :=
    presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F) (toPresheafToSheafCompComposeAndSheafify J F)
have rw : ∀ (X : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
  IsIso (X := (obj (whiskeringRight Cᵒᵖ A B) F ⋙ presheafToSheaf J B).obj X) (Y :=
    (presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F).obj X)
    (NatTrans.app (toPresheafToSheafCompComposeAndSheafify J F) X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_4 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_5 : J.PreservesSheafification F
X : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ IsIso (X := (obj (whiskeringRight Cᵒᵖ A B) F ⋙ presheafToSheaf J B).obj X) (Y :=
    (presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F).obj X)
    (NatTrans.app (toPresheafToSheafCompComposeAndSheafify J F) X)
have dsimp : IsIso (X := obj (presheafToSheaf J B) (X ⋙ F)) (Y :=
  obj (presheafToSheaf J B) ((obj (presheafToSheaf J A) X).obj (P := Presheaf.IsSheaf J) ⋙ F))
  (map (presheafToSheaf J B) (whiskerRight (toSheafify J X) F))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
⊢ J.PreservesSheafification F ↔
    ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))
have simp : J.PreservesSheafification F ↔ ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
Tactic: simp only [← J.W_iff_isIso_map_of_adjunction adj₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
⊢ J.PreservesSheafification F ↔ ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
have mp : J.PreservesSheafification F → ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
mp : J.PreservesSheafification F → ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
⊢ J.PreservesSheafification F ↔ ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
have mpr : (∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)) → J.PreservesSheafification F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ J.W (whiskerRight (adj₁.unit.app P) F)
have mp : J.W (adj₁.unit.app P)
Tactic: apply W_of_preservesSheafification
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ J.W (adj₁.unit.app P)
have mp : IsIso (G₁.map (adj₁.unit.app P))
Tactic: rw [J.W_iff_isIso_map_of_adjunction adj₁]