awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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₂
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:
exact hiso r.Z i (r.g₁ ≫ g)

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Z, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))

Tactic:
have hZ : IsIso (f.hom.app (op r.Z)) := by
        obtain ⟨i, ⟨g⟩⟩ := I₁.hf
        exact hiso r.Z i (r.g₁ ≫ g)
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
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))
⊢ 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)

Tactic:
simp only [Category.assoc, f.hom.naturality_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.NatTrans.naturality_inv
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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)))
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))
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 (r.g₂ ≫ I₂.f).op ≫ inv (f.hom.app (op r.Z))
rw₆ 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 (r.g₂ ≫ I₂.f).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))

Tactic:
rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_comp, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ IsIso (f.hom.app W)

Tactic:
⟨⟨invMap, ?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
refine_1 : f.hom.app W ≫ invMap = 𝟙 (F.obj (P := Presheaf.IsSheaf K).obj W)
refine_2 : invMap ≫ f.hom.app W = 𝟙 (G.obj (P := Presheaf.IsSheaf K).obj W)
⊢ IsIso (f.hom.app W)

Tactic:
refine ⟨⟨invMap, ?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ f.hom.app W ≫ invMap = 𝟙 (F.obj (P := Presheaf.IsSheaf K).obj W)

Tactic:
F.property.hom_ext S _ _ fun I => ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
refine_1 :
  ∀ (I : S.Arrow),
    (f.hom.app W ≫ invMap) ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op =
      𝟙 (F.obj (P := Presheaf.IsSheaf K).obj W) ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op
⊢ f.hom.app W ≫ invMap = 𝟙 (F.obj (P := Presheaf.IsSheaf K).obj W)

Tactic:
refine F.property.hom_ext S _ _ fun I => ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
refine_1 :
  f.hom.app W ≫ invMap ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op = F.obj (P := Presheaf.IsSheaf K).map I.f.op
⊢ (f.hom.app W ≫ invMap) ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op =
    𝟙 (F.obj (P := Presheaf.IsSheaf K).obj W) ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op

Tactic:
simp only [op_unop, Category.assoc, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, Opposite.op_unop, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
refine_1 :
  F.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ f.hom.app (op I.Y) ≫ inv (f.hom.app (op I.Y)) =
    F.obj (P := Presheaf.IsSheaf K).map I.f.op
⊢ f.hom.app W ≫ invMap ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op = F.obj (P := Presheaf.IsSheaf K).map I.f.op

Tactic:
rw [Presheaf.IsSheaf.amalgamate_map, ← f.hom.naturality_assoc]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ F.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ f.hom.app (op I.Y) ≫ inv (f.hom.app (op I.Y)) =
    F.obj (P := Presheaf.IsSheaf K).map I.f.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
⊢ invMap ≫ f.hom.app W = 𝟙 (G.obj (P := Presheaf.IsSheaf K).obj W)

Tactic:
G.property.hom_ext S _ _ fun I => ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
refine_2 :
  ∀ (I : S.Arrow),
    (invMap ≫ f.hom.app W) ≫ G.obj (P := Presheaf.IsSheaf K).map I.f.op =
      𝟙 (G.obj (P := Presheaf.IsSheaf K).obj W) ≫ G.obj (P := Presheaf.IsSheaf K).map I.f.op
⊢ invMap ≫ f.hom.app W = 𝟙 (G.obj (P := Presheaf.IsSheaf K).obj W)

Tactic:
refine G.property.hom_ext S _ _ fun I => ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.IsSheaf.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
refine_2 :
  invMap ≫ f.hom.app W ≫ G.obj (P := Presheaf.IsSheaf K).map I.f.op = G.obj (P := Presheaf.IsSheaf K).map I.f.op
⊢ (invMap ≫ f.hom.app W) ≫ G.obj (P := Presheaf.IsSheaf K).map I.f.op =
    𝟙 (G.obj (P := Presheaf.IsSheaf K).obj W) ≫ G.obj (P := Presheaf.IsSheaf K).map I.f.op

Tactic:
simp only [op_unop, Category.assoc, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, Opposite.op_unop, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
refine_2 :
  (G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ≫ f.hom.app (op I.Y) =
    G.obj (P := Presheaf.IsSheaf K).map I.f.op
⊢ invMap ≫ f.hom.app W ≫ G.obj (P := Presheaf.IsSheaf K).map I.f.op = G.obj (P := Presheaf.IsSheaf K).map I.f.op

Tactic:
rw [← f.hom.naturality, Presheaf.IsSheaf.amalgamate_map_assoc]

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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))
invMap : G.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) ⟶ F.obj (P := Presheaf.IsSheaf K).obj (op (unop W)) :=
  ⋯.amalgamate S (fun (I : S.Arrow) ↦ G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ (G.obj (P := Presheaf.IsSheaf K).map I.f.op ≫ inv (f.hom.app (op I.Y))) ≫ f.hom.app (op I.Y) =
    G.obj (P := Presheaf.IsSheaf K).map I.f.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
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
⊢ IsIso f ↔
    ∀ (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)

Tactic:
⟨fun _ _ => inferInstance, fun h => isIso_of_coversTop hX h⟩

Premises used: CategoryTheory.Sheaf.isIso_of_coversTop, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
h :
  Eq (α := (P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) → Prop) (Presheaf.IsSheaf J)
    fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
    Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x
⊢ Eq (α := MorphismProperty (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) J.W
    (ObjectProperty.isLocal fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
h :
  ∀ (P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A),
    Presheaf.IsSheaf J P ↔
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P
⊢ Eq (α := (P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) → Prop) (Presheaf.IsSheaf J)
    fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
    Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x

Tactic:
ext P