awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s
have w : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
  (G.sieveOfSection (↑s : F.obj U)).arrows f →
    Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s) :
        (fun (X : Type w) ↦ X) (F'.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s) :
        (fun (X : Type w) ↦ X) (F'.obj (op Y)))
Tactic: apply (h _ s.prop).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection (↑s : F.obj U)).arrows i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))
have w : Eq (α := F'.obj (op V))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
        F'.obj U) :
    F'.obj (op V))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
        F'.obj U) :
    F'.obj (op V))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection (↑s : F.obj U)).arrows i
⊢ Eq (α := F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
          F'.obj U) :
      F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
          F'.obj U) :
      F'.obj (op V))
have w : Eq (α := F'.obj (op V))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app (op V)) :
        (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
      (({
              toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                Subtype.mk (p := fun (x : F.obj (op V)) ↦
                  Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                    (↑x : F.obj U))
                  sorry } :
            (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
          s :
        (↑((sheafify J G).obj (op V)) : Type w)) :
    F'.obj (op V))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app (op V)) :
        (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
      (({
              toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                Subtype.mk (p := fun (x : F.obj (op V)) ↦
                  Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                    (↑x : F.obj U))
                  sorry } :
            (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
          s :
        (↑((sheafify J G).obj (op V)) : Type w)) :
    F'.obj (op V))
Tactic: rw [← dsimp% l₁.naturality_apply, ← dsimp% l₂.naturality_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
⊢ x ∈ G'.obj U
have h₁ : x =
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
          (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) → (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
        (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
    F.obj U)
Tactic: convert! ((G.sheafifyLift (Subfunctor.homOfLe h) hG').app U ⟨x, hx⟩).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
⊢ x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
            (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) → (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
          (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
      F.obj U)
have h₁ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
  (G.sieveOfSection x).arrows f →
    Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
                  (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                    (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
                (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
            F.obj U) :
        (fun (X : Type w) ↦ X) (F.obj (op Y)))
Tactic: apply (hF _ hx).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        x :
      (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
                (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                  (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
              (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
          F.obj U) :
      (fun (X : Type w) ↦ X) (F.obj (op V)))
have this : Eq.{w + 1} (α := F.obj (op V))
  ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                  (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
              (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                    (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                  x)
                hi)) :
          F.obj (op V)) :
        F.obj (op V)))
    (homOfLe sorry ≫ G.sheafifyLift (homOfLe h) hG'))
  ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                  (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
              (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                    (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                  x)
                hi)) :
          F.obj (op V)) :
        F.obj (op V)))
    (homOfLe h))
Tactic: have :=
    congr_arg (fun f : G.toFunctor ⟶ G'.toFunctor => (NatTrans.app f (op V) ⟨_, hi⟩).1)
      (G.to_sheafifyLift (Subfunctor.homOfLe h) hG')
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presheaf.IsSheaf J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor
have rw : Presieve.IsSheaf.{w, v, u} J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presieve.IsSheaf.{w, v, u} J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor
have hF : Presieve.IsSheaf.{w, v, u} J (F'.obj (P := Presheaf.IsSheaf J))
Tactic: apply Subfunctor.sheafify_isSheaf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presieve.IsSheaf.{w, v, u} J (F'.obj (P := Presheaf.IsSheaf J))
have hF : Presheaf.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ toImage f ≫ imageι f = f
have h : (toImage f ≫ imageι f).hom = f.hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono (X := Functor.obj (sheafToPresheaf J (Type w)) (Sheaf.image f))
    (Functor.map (sheafToPresheaf J (Type w)) (Sheaf.imageι f))
have dsimp : Mono (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Epi (Sheaf.toImage f)
have refine : ∀ (G' : Sheaf J (Type w)) (g₁ g₂ : Sheaf.image f ⟶ G') (e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂), g₁ = g₂
Tactic: refine ⟨@fun G' g₁ g₂ e => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G'_1 : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
⊢ g₁ = g₂
have h : ∀ (U : Cᵒᵖ) (s : F'.obj (P := Presheaf.IsSheaf J).obj U)
  (hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)
Tactic: ext U ⟨s, hx⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G'_1 : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj (P := Presheaf.IsSheaf J).obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)
have h : ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
  ((Subfunctor.range f.hom).sieveOfSection s).arrows f_1 →
    Eq (α := (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G'.obj (P := Presheaf.IsSheaf J).map f_1.op) :
            (a : (fun (X : Type w) ↦ X) (G'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
            (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
              x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)) :
        (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G'.obj (P := Presheaf.IsSheaf J).map f_1.op) :
            (a : (fun (X : Type w) ↦ X) (G'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
            (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
              x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)) :
        (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: apply ((isSheaf_iff_isSheaf_of_type J _).mp G'.2 _ hx).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (imageMonoFactorization f).I ⟶ I.I
have M : Mono I.m.hom
Tactic: haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J (Type (max v u)) _).mp I.m_mono
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ (imageMonoFactorization f).I ⟶ I.I
have refine : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
Tactic: refine ⟨Subfunctor.homOfLe ?_ ≫ inv (Subfunctor.toRange I.m.1)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
have h : Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom
Tactic: apply Subfunctor.sheafify_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
h : Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom
⊢ Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
have hF : Presieve.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
Tactic: apply Subfunctor.sheafify_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
h : Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom
hF : Presieve.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
⊢ Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
have hG' : Presieve.IsSheaf J (Subfunctor.range I.m.hom).toFunctor
Tactic: apply Subfunctor.sheafify_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
| Subfunctor.range f.hom
have rw : Subfunctor.range (I.e ≫ I.m).hom
Tactic: rw [← I.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom
have h : Subfunctor.range (I.e ≫ I.m).hom ≤ Subfunctor.range I.m.hom
Tactic: conv_lhs => rw [← I.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presieve.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
have hF : Presheaf.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presieve.IsSheaf J (Subfunctor.range I.m.hom).toFunctor
have hG' : Presieve.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))
Tactic: apply Presieve.isSheaf_iso J (asIso <| Subfunctor.toRange I.m.1)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presieve.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))
have hG' : Presheaf.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ { hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) :
        InducedCategory.Hom (D := Cᵒᵖ ⥤ Type (max v u)) (F :=
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) (imageMonoFactorization f).I I.I } ≫
      I.m =
    (imageMonoFactorization f).m
have h : InducedCategory.Hom.hom
    ({ hom := Subfunctor.homOfLe sorry ≫ inv (Subfunctor.toRange I.m.hom) :
        InducedCategory.Hom (D := Cᵒᵖ ⥤ Type (max v u)) (F :=
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) (imageMonoFactorization f).I I.I } ≫
      I.m) =
  (imageMonoFactorization f).m.hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom)) ≫ I.m.hom =
    (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
have h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
⊢ (Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom)) ≫ I.m.hom =
    (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
have pf : IsIso (Subfunctor.toRange I.m.hom)
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
pf : IsIso (Subfunctor.toRange I.m.hom)
⊢ (Subfunctor.homOfLe h ≫ inv (Subfunctor.toRange I.m.hom)) ≫ I.m.hom =
    (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
have h₁ : Subfunctor.homOfLe h ≫ inv (Subfunctor.toRange I.m.hom) ≫ I.m.hom = Subfunctor.homOfLe h ≫ (Subfunctor.range I.m.hom).ι
Tactic: rw [← Subfunctor.homOfLe_ι h, Category.assoc]