awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
V₃ : C
iV₃ : V₃ ⟶ V₂
e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂
⊢ Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁)).op) :
          (a : ℱ.obj.obj (op (G.obj Y₁))) → ℱ.obj.obj (op (G.obj V₃)))
        (x g₁ hg₁) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map (iV₃ ≫ iV₂Y₂)).op) :
          (a : ℱ.obj.obj (op (G.obj Y₂))) → ℱ.obj.obj (op (G.obj V₃)))
        (x g₂ hg₂) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₃)))
have compatible : (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁) ≫ g₁ = (iV₃ ≫ iV₂Y₂) ≫ g₂
Tactic: apply hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 : Sheaf.{v_2, v_4, u_2, u_4} K A
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e :
  Eq (α := obj (G.sheafPushforwardContinuous A J K) ℱ ⟶ obj (G.sheafPushforwardContinuous A J K) ℱ')
    (map (G.sheafPushforwardContinuous A J K) α) (map (G.sheafPushforwardContinuous A J K) β)
⊢ α = β
have h : α.hom = β.hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 : Sheaf.{v_2, v_4, u_2, u_4} K A
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e :
  Eq (α := obj (G.sheafPushforwardContinuous A J K) ℱ ⟶ obj (G.sheafPushforwardContinuous A J K) ℱ')
    (map (G.sheafPushforwardContinuous A J K) α) (map (G.sheafPushforwardContinuous A J K) β)
⊢ α.hom = β.hom
have e₁ : Eq (α :=
  (obj (G.sheafPushforwardContinuous A J K) ℱ).obj (P := Presheaf.IsSheaf J) ⟶
    (obj (G.sheafPushforwardContinuous A J K) ℱ').obj (P := Presheaf.IsSheaf J))
  (InducedCategory.Hom.hom (map (G.sheafPushforwardContinuous A J K) α))
  (InducedCategory.Hom.hom (map (G.sheafPushforwardContinuous A J K) β))
Tactic: apply_fun fun e => e.hom at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 : Sheaf.{v_2, v_4, u_2, u_4} K A
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
⊢ α.hom = β.hom
have h : sheafHom (G.op.whiskerLeft α.hom) = β.hom
Tactic: rw [← sheafHom_eq G α.hom, ← sheafHom_eq G β.hom, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 : Sheaf.{v_2, v_4, u_2, u_4} K A
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
h : sheafHom (G.op.whiskerLeft α.hom) = β.hom
⊢ α.hom = β.hom
have h₁ : sheafHom (G.op.whiskerLeft α.hom) = sheafHom (G.op.whiskerLeft β.hom)
Tactic: rw [← sheafHom_eq G α.hom, ← sheafHom_eq G β.hom, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 : Sheaf.{v_2, v_4, u_2, u_4} K A
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
h : sheafHom (G.op.whiskerLeft α.hom) = β.hom
h₁ : sheafHom (G.op.whiskerLeft α.hom) = sheafHom (G.op.whiskerLeft β.hom)
⊢ α.hom = β.hom
have h₂ : sheafHom (G.op.whiskerLeft β.hom) = sheafHom (G.op.whiskerLeft β.hom)
Tactic: rw [← sheafHom_eq G α.hom, ← sheafHom_eq G β.hom, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y : C
f₁ f₂ : X ⟶ Y
h : G.map f₁ = G.map f₂
W₀ : C
a : W₀ ⟶ X
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (Sieve.equalizer f₁ f₂) ⋯) :
        Sieve X).arrows
    a
⊢ F.obj (P := Presheaf.IsSheaf J).map f₁.op ≫
      F.obj (P := Presheaf.IsSheaf J).map
        { Y := W₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X)
                  (Sieve.equalizer f₁ f₂) ⋯) }.f.op =
    F.obj (P := Presheaf.IsSheaf J).map f₂.op ≫ F.obj (P := Presheaf.IsSheaf J).map { Y := W₀, f := a, hf := ha }.f.op
have dsimp : F.obj (P := Presheaf.IsSheaf J).map f₁.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
  F.obj (P := Presheaf.IsSheaf J).map f₂.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
Tactic: dsimp at ha ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Z) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Z)
            (Sieve.pullback p (G.imageSieve f)) ⋯) :
        Sieve Z).arrows
    a
⊢ (mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map p.op) ≫
      F.obj (P := Presheaf.IsSheaf J).map
        { Y := W₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Z) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Z)
                  (Sieve.pullback p (G.imageSieve f)) ⋯) }.f.op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map { Y := W₀, f := a, hf := ha }.f.op
have dsimp : (mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map p.op) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
  F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
Tactic: dsimp at ha ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
⊢ (mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map p.op) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
have rw : sorry.amalgamate (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) sorry)
      (fun
          (x :
            GrothendieckTopology.Cover.Arrow
              (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f)
                sorry)) ↦
        (match (motive :=
            (x :
                GrothendieckTopology.Cover.Arrow
                  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f)
                    sorry)) →
              F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
            x with
          | { Y := W₀, f := a, hf := ha } =>
            F.obj (P := Presheaf.IsSheaf J).map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op :
          F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y)))
      sorry ≫
    F.obj (P := Presheaf.IsSheaf J).map (a ≫ p).op =
  F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
Tactic: rw [Category.assoc, ← Functor.map_comp, ← op_comp, mapPreimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
⊢ ⋯.amalgamate (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
        (fun
            (x :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f)
                  ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X)
                      (G.imageSieve f) ⋯)) →
                F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } =>
              F.obj (P := Presheaf.IsSheaf J).map
                (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op :
            F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y)))
        ⋯ ≫
      F.obj (P := Presheaf.IsSheaf J).map (a ≫ p).op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
have rw : (match (motive :=
    (x :
        GrothendieckTopology.Cover.Arrow
          (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) sorry)) →
      F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
    { Y := W₀, f := a ≫ p, hf := ha } with
  | { Y := W₀, f := a, hf := ha } =>
    F.obj (P := Presheaf.IsSheaf J).map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op) =
  F.obj (P := Presheaf.IsSheaf J).map (a ≫ g).op
Tactic: rw [F.2.amalgamate_map ⟨_, imageSieve_mem J K G f⟩
        (fun ⟨W₀, a, ha⟩ ↦ F.obj.map ha.choose.op) _ ⟨W₀, a ≫ p, ha⟩,
        ← Functor.map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
⊢ (match (motive :=
      (x :
          GrothendieckTopology.Cover.Arrow
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)) →
        F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
      { Y := W₀, f := a ≫ p, hf := ha } with
    | { Y := W₀, f := a, hf := ha } =>
      F.obj (P := Presheaf.IsSheaf J).map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op) =
    F.obj (P := Presheaf.IsSheaf J).map (a ≫ g).op
have h : G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)
Tactic: apply map_eq_of_eq K G
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
⊢ G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)
have h : G.map (a ≫ p) ≫ f = G.map (a ≫ g)
Tactic: rw [ha.choose_spec, Functor.map_comp_assoc, Functor.map_comp, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
h : G.map (a ≫ p) ≫ f = G.map (a ≫ g)
⊢ G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)
have h₁ : G.map a ≫ G.map p ≫ f = G.map (a ≫ g)
Tactic: rw [ha.choose_spec, Functor.map_comp_assoc, Functor.map_comp, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
h : G.map (a ≫ p) ≫ f = G.map (a ≫ g)
h₁ : G.map a ≫ G.map p ≫ f = G.map (a ≫ g)
⊢ G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)
have h₂ : G.map a ≫ G.map p ≫ f = G.map a ≫ G.map g
Tactic: rw [ha.choose_spec, Functor.map_comp_assoc, Functor.map_comp, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
h : G.map (a ≫ p) ≫ f = G.map (a ≫ g)
h₁ : G.map a ≫ G.map p ≫ f = G.map (a ≫ g)
h₂ : G.map a ≫ G.map p ≫ f = G.map a ≫ G.map g
⊢ G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)
have h₃ : G.map a ≫ G.map g = G.map a ≫ G.map g
Tactic: rw [ha.choose_spec, Functor.map_comp_assoc, Functor.map_comp, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X : C
⊢ mapPreimage K G F (𝟙 (G.obj X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
have rw : mapPreimage K G F (G.map (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
Tactic: rw [← G.map_id, mapPreimage_map, op_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X : C
rw : mapPreimage K G F (G.map (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ mapPreimage K G F (𝟙 (G.obj X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
have rw₁ : F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
Tactic: rw [← G.map_id, mapPreimage_map, op_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X : C
rw : mapPreimage K G F (G.map (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
rw₁ : F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ mapPreimage K G F (𝟙 (G.obj X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
have rw₂ : F.obj (P := Presheaf.IsSheaf J).map (𝟙 (op X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
Tactic: rw [← G.map_id, mapPreimage_map, op_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X : C
rw : mapPreimage K G F (G.map (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
rw₁ : F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
rw₂ : F.obj (P := Presheaf.IsSheaf J).map (𝟙 (op X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ mapPreimage K G F (𝟙 (G.obj X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
have rw₃ : Eq.{v_4 + 1} (α := F.obj (P := Presheaf.IsSheaf J).obj (op X) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
  (𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))) (𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X)))
Tactic: rw [← G.map_id, mapPreimage_map, op_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
⊢ Eq (α :=
    F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶
      F.obj (P := Presheaf.IsSheaf J).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
            Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
            { Y := T₀, f := a, hf := ⋯ })))
    (mapPreimage K G F (f ≫ g) ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ })))
    ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ })))
have h : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} T₀) ↦ S ∈ (J : (a : C) → Set (Sieve a)) T₀)
        (Sieve.pullback b (G.imageSieve g)) sorry)),
  Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op I.Y))
    ((mapPreimage K G F (f ≫ g) ≫
        F.obj (P := Presheaf.IsSheaf J).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := sorry }))) ≫
      F.obj (P := Presheaf.IsSheaf J).map I.f.op)
    (((mapPreimage K G F g ≫ mapPreimage K G F f) ≫
        F.obj (P := Presheaf.IsSheaf J).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := sorry }))) ≫
      F.obj (P := Presheaf.IsSheaf J).map I.f.op)
Tactic: apply Presheaf.IsSheaf.hom_ext F.property
        ⟨_, J.pullback_stable b (imageSieve_mem J K G g)⟩