awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
⊢ (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible (R := Sieve.arrows (Sieve.coverByImage G (unop U)))

Tactic:
exact pushforwardFamily_compatible (homOver α Y.unop) (f.unop ≫ x)

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, CategoryTheory.CategoryStruct.comp, Opposite.unop, CategoryTheory.Functor.IsCoverDense.homOver
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
w :
  (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op =
    (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop Y))).map f'.op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop Y))).obj (op Y')))
      (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
              (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
          x) =
    pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x) f' hf'

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
w :
  Eq (α := unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op)
    (f.unop ≫
      x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op)
⊢ (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op =
    (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
w :
  Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
⊢ Eq (α := unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op)
    (f.unop ≫
      x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))

Tactic:
rw [← hf'.some.fac]

Premises used: CategoryTheory.Presieve.CoverByImageStructure.fac, Nonempty.some
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
w :
  Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
⊢ Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))

Tactic:
conv_lhs => rw [← hf'.some.fac]

Premises used: CategoryTheory.Presieve.CoverByImageStructure.fac, Nonempty.some
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
w :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op =
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op
⊢ Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))

Tactic:
simp only [← Category.assoc, op_comp, Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
w :
  Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj)))
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1) :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').1)))
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op =
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ Eq (α :=
    (fun (X : Type v_4) ↦ X)
      ((sheafOver ℱ' (unop X)).obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (homOver α (unop X)) (op (Nonempty.some hf').obj)) :
          (a : (fun (X : Type v_4) ↦ X) ((G.op ⋙ ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (Nonempty.some hf').obj))) →
            (fun (X : Type v_4) ↦ X) ((G.op ⋙ (sheafOver ℱ' (unop X)).obj).obj (op (Nonempty.some hf').obj)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((ℱ ⋙ obj coyoneda (op (unop X))).map (Nonempty.some hf').map.op) :
              (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
                (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (G.obj (Nonempty.some hf').obj))))
            x :
          (fun (X : Type v_4) ↦ X) ((ℱ ⋙ obj coyoneda (op (unop X))).obj (op (G.obj (Nonempty.some hf').obj)))) :
      (fun (X : Type v_4) ↦ X)
        ((G.op ⋙ (sheafOver ℱ' (unop X)).obj (P := Presheaf.IsSheaf K)).obj (op (Nonempty.some hf').obj)))
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1) :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').1)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj)))
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1) :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').1)))

Tactic:
exact (appHom_restrict (homOver α (unop X)) hf'.some.map.op x).trans (by simp)

Premises used: Quiver.Hom.op, Nonempty.some, CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict, CategoryTheory.Presieve.CoverByImageStructure.map, Opposite.unop, Eq.trans, CategoryTheory.Functor.IsCoverDense.homOver
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
U : Dᵒᵖ
α : coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ ⟶
  coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K)) :=
  sheafCoyonedaHom α_1
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ ((ℱ ⋙ yoneda).obj U).map f ≫ (α.app Y).app U =
    (α.app X).app U ≫ ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U).map f

Tactic:
simpa using congr_app (α.naturality f) U

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
U V : Dᵒᵖ
i : U ⟶ V
w :
  ∀ (X : Aᵒᵖ) (x : ((ℱ ⋙ yoneda).obj U).obj X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((ℱ ⋙ yoneda).map i ≫
              let α_1 := sheafCoyonedaHom α;
              { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app V, naturality := ⋯ :
                NatTrans ((ℱ ⋙ yoneda).obj V) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj V) })
            X))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((let α_1 := sheafCoyonedaHom α;
              { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app U, naturality := ⋯ :
                NatTrans ((ℱ ⋙ yoneda).obj U) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U) }) ≫
              (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).map i)
            X))
        x
⊢ ((ℱ ⋙ yoneda).map i ≫
      let α_1 := sheafCoyonedaHom α;
      { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app V, naturality := ⋯ }) =
    (let α_1 := sheafCoyonedaHom α;
      { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app U, naturality := ⋯ :
        NatTrans ((ℱ ⋙ yoneda).obj U) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U) }) ≫
      (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).map i

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
U V : Dᵒᵖ
i : U ⟶ V
X : Aᵒᵖ
x : ((ℱ ⋙ yoneda).obj U).obj X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((ℱ ⋙ yoneda).map i ≫
            let α_1 := sheafCoyonedaHom α;
            { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app V, naturality := ⋯ :
              NatTrans ((ℱ ⋙ yoneda).obj V) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj V) })
          X))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((let α_1 := sheafCoyonedaHom α;
            { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app U, naturality := ⋯ :
              NatTrans ((ℱ ⋙ yoneda).obj U) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U) }) ≫
            (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).map i)
          X))
      x

Tactic:
ConcreteCategory.congr_hom (((sheafCoyonedaHom α).app X).naturality i) x

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
U V : Dᵒᵖ
i : U ⟶ V
X : Aᵒᵖ
x : ((ℱ ⋙ yoneda).obj U).obj X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((ℱ ⋙ yoneda).map i ≫
            let α_1 := sheafCoyonedaHom α;
            { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app V, naturality := ⋯ :
              NatTrans ((ℱ ⋙ yoneda).obj V) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj V) })
          X))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((let α_1 := sheafCoyonedaHom α;
            { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app U, naturality := ⋯ :
              NatTrans ((ℱ ⋙ yoneda).obj U) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U) }) ≫
            (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).map i)
          X))
      x

Tactic:
exact ConcreteCategory.congr_hom (((sheafCoyonedaHom α).app X).naturality i) x

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom, CategoryTheory.NatTrans.app