awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
rw :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt)
rw₁ :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      toSheafify J ((F.obj k).obj (P := Presheaf.IsSheaf J)) ≫ sheafifyMap J (E.ι.app k))
rw₂ :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (sheafifyLift J (𝟙 ((F.obj k).obj (P := Presheaf.IsSheaf J))) ⋯ ≫
      toSheafify J ((F.obj k).obj (P := Presheaf.IsSheaf J)) ≫ sheafifyMap J (E.ι.app k))
⊢ 𝟙 ((Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J)) ≫
      InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)) =
    InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt
have rw₃ : Eq (α :=
  (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
    (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
  (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k))) (sheafifyMap J (E.ι.app k))
Tactic: rw [Category.id_comp, toSheafify_naturality, sheafificationAdjunction_counit_app_val,
    sheafifyLift_id_toSheafify_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const K)
          (Cocone.pt (J := K) (F := F)
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } }))
        j)
      (NatTrans.app
        (Cocone.ι
          { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
            ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
        j)
      { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) } =
    S.ι.app j
have h₁ : InducedCategory.Hom.hom
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const K)
          (Cocone.pt (J := K) (F := F)
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt sorry,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := sorry } }))
        j)
      (NatTrans.app
        (Cocone.ι
          { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt sorry,
            ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := sorry } })
        j)
      { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }) =
  (S.ι.app j).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const K)
            (Cocone.pt (J := K) (F := F)
              { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
                ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } }))
          j)
        (NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j)
        { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }) =
    (S.ι.app j).hom
have h₁ : E.ι.app j ≫ hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) = (S.ι.app j).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ E.ι.app j ≫ hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) = (S.ι.app j).hom
have h₁ : NatTrans.app (Cocone.ι (Functor.mapCocone (sheafToPresheaf J D) S)) j = (S.ι.app j).hom
Tactic: rw [hE.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m :
  Cocone.pt (J := K) (F := F)
      { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
        ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } } ⟶
    S.pt
hm :
  ∀ (j : K),
    NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j ≫
        m =
      S.ι.app j
⊢ m = { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }
have h₁ : m.hom = InducedCategory.Hom.hom { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
⊢ IsIso f
have rw : ∀ (X : Cᵒᵖ), IsIso (f.hom.app X)
Tactic: rw [← ObjectProperty.isIso_hom_iff, NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
⊢ ∀ (X : Cᵒᵖ), IsIso (f.hom.app X)
have hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
Tactic: have hiso (Z : C) (i : ι) (g : Z ⟶ X i) : IsIso (f.hom.app (op Z)) :=
    (NatTrans.isIso_iff_isIso_app ((K.overPullback A (X i)).map f).hom).mp inferInstance
      (op (Over.mk g))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
I : S.Arrow
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
have obtain : ∀ (i : ι) (g : I.Y ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
Tactic: obtain ⟨i, ⟨g⟩⟩ := I.hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
⊢ IsIso (f.hom.app W)
have harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
Tactic: have harrow (I : S.Arrow) : IsIso (f.hom.app (op I.Y)) := by
    obtain ⟨i, ⟨g⟩⟩ := I.hf
    exact hiso I.Y i g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
have obtain : ∀ (i : ι) (g : I₁.Y ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
Tactic: obtain ⟨i, ⟨g⟩⟩ := I₁.hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
⊢ Eq (α := G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op r.Z))
    ((fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) I₁ ≫
      F.obj (P := Presheaf.IsSheaf K).map r.g₁.op)
    ((fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) I₂ ≫
      F.obj (P := Presheaf.IsSheaf K).map r.g₂.op)
have hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
Tactic: have hZ : IsIso (f.hom.app (op r.Z)) := by
        obtain ⟨i, ⟨g⟩⟩ := I₁.hf
        exact hiso r.Z i (r.g₁ ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
⊢ Eq (α := G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op r.Z))
    ((fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) I₁ ≫
      F.obj (P := Presheaf.IsSheaf K).map r.g₁.op)
    ((fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) I₂ ≫
      F.obj (P := Presheaf.IsSheaf K).map r.g₂.op)
have simp : G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
  G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
Tactic: simp only [Category.assoc, f.hom.naturality_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
⊢ G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
have rw : (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
  G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
Tactic: rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
rw :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
⊢ G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
have rw₁ : (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
  (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫ inv (f.hom.app (op r.Z))
Tactic: rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
rw :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
rw₁ :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫
      inv (f.hom.app (op r.Z))
⊢ G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
have rw₂ : G.obj (P := Presheaf.IsSheaf K).map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
  (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫ inv (f.hom.app (op r.Z))
Tactic: rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
rw :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
rw₁ :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫
      inv (f.hom.app (op r.Z))
rw₂ :
  G.obj (P := Presheaf.IsSheaf K).map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
    (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫
      inv (f.hom.app (op r.Z))
⊢ G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
have rw₃ : Eq (α := G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op r.Z))
  (G.obj (P := Presheaf.IsSheaf K).map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)))
  (G.obj (P := Presheaf.IsSheaf K).map (I₂.f.op ≫ r.g₂.op) ≫ inv (f.hom.app (op r.Z)))
Tactic: rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocalProperties (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
rw :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
rw₁ :
  (G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op) ≫
      inv (f.hom.app (op r.Z)) =
    (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫
      inv (f.hom.app (op r.Z))
rw₂ :
  G.obj (P := Presheaf.IsSheaf K).map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
    (G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op) ≫
      inv (f.hom.app (op r.Z))
rw₃ :
  Eq (α := G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op r.Z))
    (G.obj (P := Presheaf.IsSheaf K).map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)))
    (G.obj (P := Presheaf.IsSheaf K).map (I₂.f.op ≫ r.g₂.op) ≫ inv (f.hom.app (op r.Z)))
⊢ G.obj (P := Presheaf.IsSheaf K).map I₁.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
    G.obj (P := Presheaf.IsSheaf K).map I₂.f.op ≫ G.obj (P := Presheaf.IsSheaf K).map r.g₂.op ≫ inv (f.hom.app (op r.Z))
have rw₄ : G.obj (P := Presheaf.IsSheaf K).map (r.g₁ ≫ I₁.f).op ≫ inv (f.hom.app (op r.Z)) =
  G.obj (P := Presheaf.IsSheaf K).map (I₂.f.op ≫ r.g₂.op) ≫ inv (f.hom.app (op r.Z))
Tactic: rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]