awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
G : Functor.{v_1, v_2, u_1, u_2} C D
U Y Z_1 : D
f : Y ⟶ U
h : Presieve.coverByImage G U f
g : Z_1 ⟶ Y
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f
⊢ (g ≫ f₁) ≫ f₂ = g ≫ f
have rw : g ≫ f₁ ≫ f₂ = g ≫ f
Tactic: rw [Category.assoc, ← e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
G : Functor.{v_1, v_2, u_1, u_2} C D
U Y Z_1 : D
f : Y ⟶ U
h : Presieve.coverByImage G U f
g : Z_1 ⟶ Y
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f
rw : g ≫ f₁ ≫ f₂ = g ≫ f
⊢ (g ≫ f₁) ≫ f₂ = g ≫ f
have rw₁ : g ≫ f₁ ≫ f₂ = g ≫ f₁ ≫ f₂
Tactic: rw [Category.assoc, ← e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
⊢ Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B
have obtain : ∀ (X : C) (f : G.obj X ⟶ B) (h : Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B),
  Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B
Tactic: obtain ⟨X, f, h⟩ := h B
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
⊢ Sieve.coverByImage G B ∈ (K : (a : D) → Set (Sieve a)) B
have refine : Sieve.generate (Presieve.singleton f) ≤ Sieve.coverByImage G B
Tactic: refine K.superset_covering ?_ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f_1 : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f_1) ∈ (K : (a : D) → Set (Sieve a)) B
Y : D
f : Y ⟶ B
⊢ (Sieve.generate (Presieve.singleton f_1)).arrows f → (Sieve.coverByImage G B).arrows f
have this : ∀ (Z : D) (g : Y ⟶ Z) (w : Z ⟶ B) (h : Presieve.singleton f_1 w) (w : g ≫ w = f), (Sieve.coverByImage G B).arrows f
Tactic: ⟨Z, g, _, h, w⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
K : GrothendieckTopology.{v_2, u_2} D
h_1 : ∀ (B : D), ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ (K : (a : D) → Set (Sieve a)) B
B : D
X : C
f_1 : G.obj X ⟶ B
h_2 : Sieve.generate (Presieve.singleton f_1) ∈ (K : (a : D) → Set (Sieve a)) B
Y : D
f : Y ⟶ B
Z : D
g : Y ⟶ Z
w_1 : Z ⟶ B
h : Presieve.singleton f_1 w_1
w : g ≫ w_1 = f
⊢ (Sieve.coverByImage G B).arrows f
have mk : ∀ (g : Y ⟶ G.obj X) (w : g ≫ f_1 = f), (Sieve.coverByImage G B).arrows f
Tactic: cases h
Cleared hypotheses: Z, g, w_1, h, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
ℱ : Sheaf K (Type u_5)
X : D
s t : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)
h :
  ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          s :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          t :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
⊢ s = t
have apply : ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄,
  (Sieve.coverByImage G X).arrows f →
    Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op Y)))
          s :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op Y)))
          t :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op Y)))
Tactic: apply ((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property
    (Sieve.coverByImage G X) (G.is_cover_of_isCoverDense K X)).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
    (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))
have refine : ∀ (Y : D) (iYX : Y ⟶ G.obj X) (hiYX : (↑T : Sieve (G.obj X)).arrows iYX),
  Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))) ∈
    (K : (a : D) → Set (Sieve a)) Y
Tactic: refine K.transitive T.2 _ fun Y iYX hiYX ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
⊢ Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))) ∈
    (K : (a : D) → Set (Sieve a)) Y
have apply : ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ Y⦄,
  (Sieve.coverByImage G Y).arrows f →
    Sieve.pullback f
        (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))) ∈
      (K : (a : D) → Set (Sieve a)) Y_1
Tactic: apply K.transitive (G.is_cover_of_isCoverDense _ _) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback (iWZ ≫ iZY)
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))) ∈
    (K : (a : D) → Set (Sieve a)) W
have rw : Sieve.pullback iWZ
    (Sieve.pullback iZY
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))) ∈
  (K : (a : D) → Set (Sieve a)) W
Tactic: rw [Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY
        (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))) ∈
    (K : (a : D) → Set (Sieve a)) W
have hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
  (Sieve.pullback iZY
    (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))))
Tactic: apply K.pullback_stable
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback iZY
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))))
have apply : Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤
  Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))
Tactic: apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
⊢ α.app (op Y) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map i.op = ℱ.map i.op ≫ α.app (op X)
have h : ∀ (x : (G.op ⋙ ℱ).obj (op Y)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map i.op)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op ≫ α.app (op X))).toFun x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ pushforwardFamily α x f ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
        (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y))))
          x :
        (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y))))
have simp : Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some sorry).lift.op) :
        (a : ℱ'.obj.obj (op (G.obj (Nonempty.some sorry).1))) → ℱ'.obj.obj (op (G.obj Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op (Nonempty.some sorry).1)) :
            (a : (G.op ⋙ ℱ).obj (op (Nonempty.some sorry).1)) → (G.op ⋙ ℱ'.obj).obj (op (Nonempty.some sorry).1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (Nonempty.some sorry).map.op) :
                (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj (Nonempty.some sorry).1)))
              x :
            ℱ.obj (op (G.obj (Nonempty.some sorry).1))) :
        (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op (Nonempty.some sorry).1)) :
    ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) : (a : (G.op ⋙ ℱ).obj (op Y)) → (G.op ⋙ ℱ'.obj).obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f.op) : (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj Y))) x :
        ℱ.obj (op (G.obj Y))) :
    (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))
Tactic: simp only [pushforwardFamily_def, op_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some ⋯).lift.op) :
          (a : ℱ'.obj.obj (op (G.obj (Nonempty.some ⋯).1))) → ℱ'.obj.obj (op (G.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op (Nonempty.some ⋯).1)) :
              (a : (G.op ⋙ ℱ).obj (op (Nonempty.some ⋯).1)) → (G.op ⋙ ℱ'.obj).obj (op (Nonempty.some ⋯).1))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (Nonempty.some ⋯).map.op) :
                  (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj (Nonempty.some ⋯).1)))
                x :
              ℱ.obj (op (G.obj (Nonempty.some ⋯).1))) :
          (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op (Nonempty.some ⋯).1)) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
          (a : (G.op ⋙ ℱ).obj (op Y)) → (G.op ⋙ ℱ'.obj).obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f.op) : (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj Y))) x :
          ℱ.obj (op (G.obj Y))) :
      (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))
have generalize : ∀ (l : CoverByImageStructure G f),
  Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map l.lift.op) :
          (a : ℱ'.obj.obj (op (G.obj l.1))) → ℱ'.obj.obj (op (G.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op l.1)) :
              (a : (G.op ⋙ ℱ).obj (op l.1)) → (G.op ⋙ ℱ'.obj).obj (op l.1))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map l.map.op) : (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj l.1)))
                x :
              ℱ.obj (op (G.obj l.1))) :
          (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op l.1)) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
          (a : (G.op ⋙ ℱ).obj (op Y)) → (G.op ⋙ ℱ'.obj).obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f.op) : (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj Y))) x :
          ℱ.obj (op (G.obj Y))) :
      (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))
Tactic: generalize Nonempty.some (Presieve.in_coverByImage G f) = l
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
⊢ (pushforwardFamily α x).Compatible (R := coverByImage G X)
have suffices : ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
  iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
    Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₁.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₁)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₁)) :
                (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₁))) →
                  (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₁)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₁.op) :
                    (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁))))
                  x :
                (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁)))) :
            (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₁))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₂.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₂)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₂)) :
                (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₂))) →
                  (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₂)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₂.op) :
                    (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂))))
                  x :
                (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂)))) :
            (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₂))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
Tactic: suffices ∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁)
      (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x)) by
    rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e
    simp only [pushforwardFamily, ← Functor.map_comp_apply, ← op_comp]
    generalize Nonempty.some h₁ = l₁
    generalize Nonempty.some h₂ = l₂
    obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁
    obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂
    exact this _ _ _ _ (by simpa only [Category.assoc] using e)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
⊢ appHom α X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f = ℱ.map f ≫ α.app (op Y)
have h : ∀ (x : ℱ.obj (op X)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ α.app (op Y))).toFun x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
⊢ appHom i.hom X ≫ appHom i.inv X = 𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))
have h : ∀ (x : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
x : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x
have h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
  Eq (α := (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
Tactic: apply Functor.IsCoverDense.ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
⊢ appHom i.inv X ≫ appHom i.hom X = 𝟙 (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X))
have h : ∀ (x : ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.inv X ≫ appHom i.hom X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x
Tactic: ext x