awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve U
⊢ Eq (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)
    ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        (functorPushforward (Over.post F) S) :
      Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)
    (functorPushforward F ((overEquiv U : (a : Sieve U) → Sieve U.left) S) : Sieve.{v_1, u_1} (F.obj U.left))

Tactic:
simp [Sieve.overEquiv, ← Sieve.functorPushforward_comp, ← Over.post_forget_eq_forget_comp]

Premises used: CategoryTheory.Sieve.overEquiv, CategoryTheory.Sieve.functorPushforward_comp, CategoryTheory.Over.post_forget_eq_forget_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
⊢ Membership.mem (γ := Set (Sieve Y))
    (Set.preimage (β := Sieve.{v, u} Y.left) (⇑(Sieve.overEquiv Y) : (a : Sieve Y) → Sieve Y.left)
      ((J : (a : C) → Set (Sieve a)) Y.left))
    ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ :
  Membership.mem (γ := Set (Sieve Y₁))
    (Set.preimage (β := Sieve.{v, u} Y₁.left) (⇑(Sieve.overEquiv Y₁) : (a : Sieve Y₁) → Sieve Y₁.left)
      ((J : (a : C) → Set (Sieve a)) Y₁.left))
    S₁
rw :
  Membership.mem (γ := Set (Sieve.{v, u} Y₂.left)) ((J : (a : C) → Set (Sieve a)) Y₂.left)
    (Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) S₁))
⊢ Membership.mem (γ := Set (Sieve Y₂))
    (Set.preimage (β := Sieve.{v, u} Y₂.left) (⇑(Sieve.overEquiv Y₂) : (a : Sieve Y₂) → Sieve Y₂.left)
      ((J : (a : C) → Set (Sieve a)) Y₂.left))
    (Sieve.pullback f S₁)

Tactic:
rw [Set.mem_preimage, Sieve.overEquiv_pullback]

Premises used: CategoryTheory.Sieve.overEquiv_pullback, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ :
  Membership.mem (γ := Set (Sieve Y₁))
    (Set.preimage (β := Sieve.{v, u} Y₁.left) (⇑(Sieve.overEquiv Y₁) : (a : Sieve Y₁) → Sieve Y₁.left)
      ((J : (a : C) → Set (Sieve a)) Y₁.left))
    S₁
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y₂.left)) ((J : (a : C) → Set (Sieve a)) Y₂.left)
    (Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) S₁))

Tactic:
J.pullback_stable _ h₁

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ :
  Membership.mem (γ := Set (Sieve Y₁))
    (Set.preimage (β := Sieve.{v, u} Y₁.left) (⇑(Sieve.overEquiv Y₁) : (a : Sieve Y₁) → Sieve Y₁.left)
      ((J : (a : C) → Set (Sieve a)) Y₁.left))
    S₁
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y₂.left)) ((J : (a : C) → Set (Sieve a)) Y₂.left)
    (Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) S₁))

Tactic:
exact J.pullback_stable _ h₁

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
hS :
  Membership.mem (γ := Set (Sieve Y))
    (Set.preimage (β := Sieve.{v, u} Y.left) (⇑(Sieve.overEquiv Y) : (a : Sieve Y) → Sieve Y.left)
      ((J : (a : C) → Set (Sieve a)) Y.left))
    S
R : Sieve Y
hR :
  ∀ ⦃Y_1 : Over.{v, u} X⦄ ⦃f : Y_1 ⟶ Y⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y_1))
        (Set.preimage (β := Sieve.{v, u} Y_1.left) (⇑(Sieve.overEquiv Y_1) : (a : Sieve Y_1) → Sieve Y_1.left)
          ((J : (a : C) → Set (Sieve a)) Y_1.left))
        (Sieve.pullback f R)
Z : C
f : Z ⟶ Y.left
hf : Sieve.arrows ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) S) f
⊢ Membership.mem (γ := Set (Sieve (Over.mk (f ≫ Y.hom))))
    (Set.preimage (β := Sieve.{v, u} (Over.mk (f ≫ Y.hom)).left)
      (⇑(Sieve.overEquiv (Over.mk (f ≫ Y.hom))) : (a : Sieve (Over.mk (f ≫ Y.hom))) → Sieve (Over.mk (f ≫ Y.hom)).left)
      ((J : (a : C) → Set (Sieve a)) (Over.mk (f ≫ Y.hom)).left))
    (Sieve.pullback (Over.homMk f ⋯) R)

Tactic:
specialize hR ((Sieve.overEquiv_iff _ _).1 hf)

Premises used: Iff.mp, CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
hS :
  Membership.mem (γ := Set (Sieve Y))
    (Set.preimage (β := Sieve.{v, u} Y.left) (⇑(Sieve.overEquiv Y) : (a : Sieve Y) → Sieve Y.left)
      ((J : (a : C) → Set (Sieve a)) Y.left))
    S
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hf : Sieve.arrows ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) S) f
hR :
  Membership.mem (γ := Set (Sieve (Over.mk (f ≫ Y.hom))))
    (Set.preimage (β := Sieve.{v, u} (Over.mk (f ≫ Y.hom)).left)
      (⇑(Sieve.overEquiv (Over.mk (f ≫ Y.hom))) : (a : Sieve (Over.mk (f ≫ Y.hom))) → Sieve (Over.mk (f ≫ Y.hom)).left)
      ((J : (a : C) → Set (Sieve a)) (Over.mk (f ≫ Y.hom)).left))
    (Sieve.pullback (Over.homMk f ⋯) R)
rwa :
  ∀
    (hR :
      Membership.mem (α := Sieve.{v, u} (Over.mk (f ≫ Y.hom)).left) (γ := Set (Sieve.{v, u} (Over.mk (f ≫ Y.hom)).left))
        ((J : (a : C) → Set (Sieve a)) (Over.mk (f ≫ Y.hom)).left)
        ((Sieve.overEquiv (Over.mk (f ≫ Y.hom)) : (a : Sieve (Over.mk (f ≫ Y.hom))) → Sieve (Over.mk (f ≫ Y.hom)).left)
            (Sieve.pullback (Over.homMk f ⋯) R) :
          Sieve.{v, u} (Over.mk (f ≫ Y.hom)).left)),
    Sieve.pullback f ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) R) ∈ (J : (a : C) → Set (Sieve a)) Z
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hR :
      Membership.mem (γ := Set (Sieve.{v, u} (Over.mk (f ≫ Y.hom)).left))
        ((J : (a : C) → Set (Sieve a)) (Over.mk (f ≫ Y.hom)).left)
        (Sieve.pullback (X := Y.left) (Over.Hom.left (Over.homMk f ⋯))
          ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) R))),
    Sieve.pullback f ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) R) ∈ (J : (a : C) → Set (Sieve a)) Z
⊢ Sieve.pullback f ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) R) ∈ (J : (a : C) → Set (Sieve a)) Z

Tactic:
rwa [Set.mem_preimage, Sieve.overEquiv_pullback] at hR

Premises used: CategoryTheory.Sieve.overEquiv_pullback, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
⊢ S ∈ (J.over X : (a : Over X) → Set (Sieve a)) Y ↔
    Membership.mem (α := Sieve.{v, u} Y.left) (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left)
      ((Sieve.overEquiv Y : (a : Sieve Y) → Sieve Y.left) S : Sieve.{v, u} Y.left)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
hS : Membership.mem (γ := Set (Sieve.{v, u} Y.left)) ((J : (a : C) → Set (Sieve a)) Y.left) S
⊢ Membership.mem (α := Sieve Y) ((J.over X : (a : Over X) → Set (Sieve a)) Y)
    (((Sieve.overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) S : Sieve Y)

Tactic:
simpa only [mem_over_iff, Equiv.apply_symm_apply] using hS

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
x : Sheaf J (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x_2 : Presieve.FamilyOfElements (Functor.op (Over.forget X) ⋙ x.obj (P := Presheaf.IsSheaf J)) x_1
hx : x_2.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : C
f₁ : W ⟶ Functor.obj (Over.forget X) Y₁
f₂ : W ⟶ Functor.obj (Over.forget X) Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ Functor.map (Over.forget X) g₁ = f₂ ≫ Functor.map (Over.forget X) g₂
W' : Over.{v, u} X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
⊢ f₂ ≫ Y₂.hom = W'.hom

Tactic:
simpa using h.symm =≫ Z.hom

Premises used: Eq.symm, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
x : Sheaf J (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x_2 : Presieve.FamilyOfElements (Functor.op (Over.forget X) ⋙ x.obj (P := Presheaf.IsSheaf J)) x_1
hx : x_2.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : C
f₁ : W ⟶ Functor.obj (Over.forget X) Y₁
f₂ : W ⟶ Functor.obj (Over.forget X) Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ Functor.map (Over.forget X) g₁ = f₂ ≫ Functor.map (Over.forget X) g₂
W' : Over.{v, u} X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯
h₁ : Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)
⊢ g₁' ≫ g₁ = g₂' ≫ g₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
x : Sheaf J (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x_2 : Presieve.FamilyOfElements (Functor.op (Over.forget X) ⋙ x.obj (P := Presheaf.IsSheaf J)) x_1
hx : x_2.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : C
f₁ : W ⟶ Functor.obj (Over.forget X) Y₁
f₂ : W ⟶ Functor.obj (Over.forget X) Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ Functor.map (Over.forget X) g₁ = f₂ ≫ Functor.map (Over.forget X) g₂
W' : Over.{v, u} X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
x : Sheaf J (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x_2 : Presieve.FamilyOfElements (Functor.op (Over.forget X) ⋙ x.obj (P := Presheaf.IsSheaf J)) x_1
hx : x_2.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : C
f₁ : W ⟶ Functor.obj (Over.forget X) Y₁
f₂ : W ⟶ Functor.obj (Over.forget X) Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ Functor.map (Over.forget X) g₁ = f₂ ≫ Functor.map (Over.forget X) g₂
W' : Over.{v, u} X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (x.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.obj (P := Presheaf.IsSheaf J).map f₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (x.obj.obj (Opposite.op ((Over.forget X).obj Y₁)))) →
            (fun (X : Type u_1) ↦ X) (x.obj.obj (Opposite.op W)))
        (x_2 g₁ hg₁) :
      (fun (X : Type u_1) ↦ X) (x.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.obj (P := Presheaf.IsSheaf J).map f₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (x.obj.obj (Opposite.op ((Over.forget X).obj Y₂)))) →
            (fun (X : Type u_1) ↦ X) (x.obj.obj (Opposite.op W)))
        (x_2 g₂ hg₂) :
      (fun (X : Type u_1) ↦ X) (x.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))

Tactic:
exact hx g₁' g₂' hg₁ hg₂ (by ext; exact h)
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
⊢ Functor.IsContinuous (Over.forget X) (J.over X) J

Tactic:
Functor.isContinuous_of_coverPreserving
    (over_forget_compatiblePreserving J X)
    (over_forget_coverPreserving J X)

Premises used: CategoryTheory.Functor.isContinuous_of_coverPreserving, CategoryTheory.GrothendieckTopology.over_forget_compatiblePreserving, CategoryTheory.GrothendieckTopology.over_forget_coverPreserving
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve U
hS : S ∈ (J.over X : (a : Over X) → Set (Sieve a)) U
obtain :
  ∀ (S : Sieve.{v, u} U.left)
    (hS :
      Membership.mem (α := Sieve U) ((J.over X : (a : Over X) → Set (Sieve a)) U)
        (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) S : Sieve U)),
    Membership.mem (γ := Set (Sieve ((Over.map f).obj U)))
      ((J.over Y : (a : Over Y) → Set (Sieve a)) ((Over.map f).obj U))
      (Sieve.functorPushforward (Over.map f) (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) S))
⊢ Membership.mem (γ := Set (Sieve ((Over.map f).obj U)))
    ((J.over Y : (a : Over Y) → Set (Sieve a)) ((Over.map f).obj U)) (Sieve.functorPushforward (Over.map f) S)

Tactic:
obtain ⟨S, rfl⟩ := (Sieve.overEquiv U).symm.surjective S

Premises used: CategoryTheory.Sieve.overEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve.{v, u} U.left
hS :
  Membership.mem (α := Sieve U) ((J.over X : (a : Over X) → Set (Sieve a)) U)
    (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) S : Sieve U)
rw :
  Membership.mem (α := Sieve ((Over.map f).obj U)) (γ := Set (Sieve ((Over.map f).obj U)))
    ((J.over Y : (a : Over Y) → Set (Sieve a)) ((Over.map f).obj U))
    (((Sieve.overEquiv ((Over.map f).obj U)).symm : (a : Sieve ((Over.map f).obj U).left) → Sieve ((Over.map f).obj U))
        S :
      Sieve ((Over.map f).obj U))
⊢ Membership.mem (γ := Set (Sieve ((Over.map f).obj U)))
    ((J.over Y : (a : Over Y) → Set (Sieve a)) ((Over.map f).obj U))
    (Sieve.functorPushforward (Over.map f) (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) S))

Tactic:
rw [Sieve.functorPushforward_over_map]

Premises used: CategoryTheory.Sieve.functorPushforward_over_map
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve.{v, u} U.left
hS :
  Membership.mem (α := Sieve U) ((J.over X : (a : Over X) → Set (Sieve a)) U)
    (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) S : Sieve U)
hS₁ :
  Membership.mem (γ := Set (Sieve.{v, u} ((Over.map f).obj U).left))
    ((J : (a : C) → Set (Sieve a)) ((Over.map f).obj U).left) S
⊢ Membership.mem (α := Sieve ((Over.map f).obj U)) (γ := Set (Sieve ((Over.map f).obj U)))
    ((J.over Y : (a : Over Y) → Set (Sieve a)) ((Over.map f).obj U))
    (((Sieve.overEquiv ((Over.map f).obj U)).symm : (a : Sieve ((Over.map f).obj U).left) → Sieve ((Over.map f).obj U))
        S :
      Sieve ((Over.map f).obj U))

Tactic:
apply overEquiv_symm_mem_over

Premises used: CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve.{v, u} U.left
hS :
  Membership.mem (α := Sieve U) ((J.over X : (a : Over X) → Set (Sieve a)) U)
    (((Sieve.overEquiv U).symm : (a : Sieve U.left) → Sieve U) S : Sieve U)
⊢ Membership.mem (γ := Set (Sieve.{v, u} ((Over.map f).obj U).left))
    ((J : (a : C) → Set (Sieve a)) ((Over.map f).obj U).left) S

Tactic:
simpa [mem_over_iff] using hS

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
⊢ Over.Hom.left f₂ ≫ Y₂.hom = W'.hom

Tactic:
simpa using (Over.forget _).congr_map h.symm =≫ Z.hom

Premises used: CategoryTheory.Over.forget, CategoryTheory.Functor.congr_map, Eq.symm, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
⊢ Iso.hom (Iso.refl ((Over.map f).obj W').left) ≫ W.hom = ((Over.map f).obj W').hom

Tactic:
simpa [W'] using (Over.w f₁).symm

Premises used: CategoryTheory.Over.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)
⊢ g₁' ≫ g₁ = g₂' ≫ g₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)

Tactic:
(Over.forget _).congr_map h

Premises used: CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.Over.forget, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)

Tactic:
exact (Over.forget _).congr_map h

Premises used: CategoryTheory.Over.forget, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  Eq (α := F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₁))) → F.obj.obj (Opposite.op W))
        (x g₁ hg₁) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf (J.over Y)).map
              (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₁))) → F.obj.obj (Opposite.op W))
        (x g₁ hg₁) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₁))) → F.obj.obj (Opposite.op W))
        (x g₁ hg₁) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf (J.over Y)).map (Over.isoMk (Iso.refl W.left) ⋯).inv.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj (Over.mk (Over.Hom.left f₁ ≫ Y₁.hom))))) →
            F.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.obj (P := Presheaf.IsSheaf (J.over Y)).map ((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op) :
              (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₁))) →
                F.obj.obj (Opposite.op ((Over.map f).obj (Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)))))
            (x g₁ hg₁) :
          F.obj (P := Presheaf.IsSheaf (J.over Y)).obj
            (Opposite.op ((Over.map f).obj (Over.mk (Over.Hom.left f₁ ≫ Y₁.hom))))) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))

Tactic:
rw [← Functor.map_comp_apply]

Premises used: CategoryTheory.Functor.map_comp_apply