awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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))
⊢ 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 (r.g₂ ≫ I₂.f).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)))
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))
⊢ 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 (r.g₂ ≫ I₂.f).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))
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)
have refine_1 : f.hom.app W ≫ invMap = 𝟙 (F.obj (P := Presheaf.IsSheaf K).obj W)
Tactic: refine ⟨⟨invMap, ?_, ?_⟩⟩
-- 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))
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)
⊢ IsIso (f.hom.app W)
have refine_2 : invMap ≫ f.hom.app W = 𝟙 (G.obj (P := Presheaf.IsSheaf K).obj W)
Tactic: refine ⟨⟨invMap, ?_, ?_⟩⟩
-- 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))
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)
have 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
Tactic: refine F.property.hom_ext S _ _ fun I => ?_
-- 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))
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.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
have 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
Tactic: simp only [op_unop, Category.assoc, Category.id_comp]
-- 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))
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.hom.app W ≫ invMap ≫ F.obj (P := Presheaf.IsSheaf K).map I.f.op = F.obj (P := Presheaf.IsSheaf K).map I.f.op
have 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
Tactic: rw [Presheaf.IsSheaf.amalgamate_map, ← f.hom.naturality_assoc]
-- 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))
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)
have 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
Tactic: refine G.property.hom_ext S _ _ fun I => ?_
-- 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))
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
⊢ (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
have 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
Tactic: simp only [op_unop, Category.assoc, Category.id_comp]
-- 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))
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
⊢ 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
have 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
Tactic: rw [← f.hom.naturality, Presheaf.IsSheaf.amalgamate_map_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
⊢ 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)
have 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
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
⊢ 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
have 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
Tactic: ext P
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
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
have h : 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
h :
  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
⊢ 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
have h₁ : Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P →
  Presheaf.IsSheaf J P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
F₁ F₂ : Sheaf.{v_1, v_2, u_1, u_2} J A
φ : F₁ ⟶ F₂
⊢ J.W (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ
have rw : 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
    (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔
  IsIso φ
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩, isIso_iff_of_reflects_iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
F₁ F₂ : Sheaf.{v_1, v_2, u_1, u_2} J A
φ : F₁ ⟶ F₂
rw :
  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
      (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔
    IsIso φ
⊢ J.W (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ
have rw₁ : IsIso (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩, isIso_iff_of_reflects_iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
F₁ F₂ : Sheaf.{v_1, v_2, u_1, u_2} J A
φ : F₁ ⟶ F₂
rw :
  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
      (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔
    IsIso φ
rw₁ : IsIso (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ
⊢ J.W (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ
have rw₂ : IsIso φ ↔ IsIso φ
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩, isIso_iff_of_reflects_iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
⊢ J.W (adj.unit.app P)
have rw : 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)
  (adj.unit.app P)
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
f : P₁ ⟶ P₂
⊢ J.W f ↔ IsIso (G.map f)
have rw : 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)
    f ↔
  IsIso (G.map f)
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
⊢ J.W = MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
have rw : (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) =
  MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
rw :
  (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) =
    MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
⊢ J.W = MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
have rw₁ : MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G =
  MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj]