awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
h :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
          (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯)),
    (liftAux hF α s f ≫ F.map a.op) ≫ F.map I.f.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map I.f.op
⊢ liftAux hF α s f ≫ F.map a.op = liftAux hF α s f' ≫ F.map b.op

Tactic:
apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable (G.map a ≫ f) S.2)⟩

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.cover_lift, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
h : (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
⊢ (liftAux hF α s f ≫ F.map a.op) ≫
      F.map
        { Y := T, f := g, hf := hg :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
                  (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) }.f.op =
    (liftAux hF α s f' ≫ F.map b.op) ≫ F.map { Y := T, f := g, hf := hg }.f.op

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
⊢ 𝟙 (G.obj T) ≫ { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg : S.Arrow }.f = G.map (g ≫ a) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
⊢ liftAux hF α s f ≫ F.map (g ≫ a).op =
    s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)

Tactic:
have eq₁ := liftAux_map hF α s f (g ≫ a) ⟨_, _, hg⟩ (𝟙 _) (by simp)
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  liftAux hF α s f ≫ F.map (g ≫ a).op =
    s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)
⊢ 𝟙 (G.obj T) ≫ { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg : S.Arrow }.f = G.map (g ≫ b) ≫ f'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  liftAux hF α s f ≫ F.map (g ≫ a).op =
    s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)
⊢ liftAux hF α s f' ≫ F.map (g ≫ b).op =
    s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)

Tactic:
have eq₂ := liftAux_map hF α s f' (g ≫ b) ⟨_, _, hg⟩ (𝟙 _) (by simp [w])
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  Eq (α := s.pt ⟶ F.obj (op T)) (liftAux hF α s f ≫ F.map (a.op ≫ g.op))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T))
eq₂ :
  Eq (α := s.pt ⟶ F.obj (op T)) (liftAux hF α s f' ≫ F.map (b.op ≫ g.op))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T))
⊢ liftAux hF α s f ≫ F.map a.op ≫ F.map g.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj T)))
      (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } :
        s.pt ⟶ (S.index R).left { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg })
      (α.app (op T))

Tactic:
simp only [Functor.map_comp, Functor.map_id, Category.id_comp] at eq₁ eq₂

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  Eq (α := s.pt ⟶ F.obj (op T)) (liftAux hF α s f ≫ F.map (a.op ≫ g.op))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T))
eq₂ :
  Eq (α := s.pt ⟶ F.obj (op T)) (liftAux hF α s f' ≫ F.map (b.op ≫ g.op))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T))
eq₃ :
  liftAux hF α s f ≫ F.map a.op ≫ F.map g.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj T)))
      (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } :
        s.pt ⟶ (S.index R).left { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg })
      (α.app (op T))
⊢ liftAux hF α s f' ≫ F.map b.op ≫ F.map g.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj T)))
      (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } :
        s.pt ⟶ (S.index R).left { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg })
      (α.app (op T))

Tactic:
simp only [Functor.map_comp, Functor.map_id, Category.id_comp] at eq₁ eq₂

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  liftAux hF α s f ≫ F.map a.op ≫ F.map g.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj T)))
      (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } :
        s.pt ⟶ (S.index R).left { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg })
      (α.app (op T))
eq₂ :
  liftAux hF α s f' ≫ F.map b.op ≫ F.map g.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj T)))
      (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } :
        s.pt ⟶ (S.index R).left { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg })
      (α.app (op T))
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op

Tactic:
simp only [Category.assoc, eq₁, eq₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j j' : StructuredArrow (op X) G.op
φ : j ⟶ j'
⊢ (G.map (𝟙 (unop j'.right)) ≫ j'.hom.unop).op = (G.map (StructuredArrow.Hom.right φ).unop ≫ j.hom.unop).op

Tactic:
simpa using (StructuredArrow.w φ).symm

Premises used: CategoryTheory.StructuredArrow.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j j' : StructuredArrow (op X) G.op
φ : j ⟶ j'
⊢ Functor.map (Functor.obj (Functor.const (StructuredArrow (op X) G.op)) s.1) φ ≫ liftAux hF α s j'.hom.unop =
    liftAux hF α s j.hom.unop ≫ (StructuredArrow.proj (op X) G.op ⋙ F).map φ

Tactic:
simpa using liftAux_map' hF α s j'.hom.unop j.hom.unop (𝟙 _) φ.right.unop
          (Quiver.Hom.op_inj (by simpa using (StructuredArrow.w φ).symm))

Premises used: CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map', Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.CategoryStruct.id, CategoryTheory.StructuredArrow.hom, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j : StructuredArrow (op X) G.op
⊢ lift hF hR s ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s j.hom.unop

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
apply :
  ∀ (j : StructuredArrow (op i.Y) G.op),
    Eq (α := s.pt ⟶ (StructuredArrow.proj (op i.Y) G.op ⋙ F).obj j)
      ((lift hF hR s ≫ R.map i.f.op) ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op i.Y))) j)
      (s.ι i ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op i.Y))) j)
⊢ lift hF hR s ≫ R.map i.f.op = s.ι i

Tactic:
apply (hR (op i.Y)).hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, Opposite.op, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
⊢ Eq (α := s.pt ⟶ F.obj (StructuredArrow.right (S := op X) (StructuredArrow.mk (i.f.op ≫ j.hom))))
    (lift hF hR s ≫
      R.map (StructuredArrow.hom (StructuredArrow.mk (i.f.op ≫ j.hom))) ≫
        α.app (StructuredArrow.right (S := op X) (StructuredArrow.mk (i.f.op ≫ j.hom))))
    (liftAux hF α s (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (i.f.op ≫ j.hom)))))

Tactic:
have eq := fac' hF hR s (StructuredArrow.mk (i.f.op ≫ j.hom))
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq :
  Eq (α := s.pt ⟶ F.obj (StructuredArrow.right (S := op X) (StructuredArrow.mk (i.f.op ≫ j.hom))))
    (lift hF hR s ≫
      R.map (StructuredArrow.hom (StructuredArrow.mk (i.f.op ≫ j.hom))) ≫
        α.app (StructuredArrow.right (S := op X) (StructuredArrow.mk (i.f.op ≫ j.hom))))
    (liftAux hF α s (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (i.f.op ≫ j.hom)))))
dsimp : (lift hF hR s ≫ R.map i.f.op) ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right
⊢ Eq (α := s.pt ⟶ (StructuredArrow.proj (op i.Y) G.op ⋙ F).obj j)
    ((lift hF hR s ≫ R.map i.f.op) ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op i.Y))) j)
    (s.ι i ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op i.Y))) j)

Tactic:
dsimp at eq ⊢
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map (i.f.op ≫ j.hom) ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)

Tactic:
simp only [Functor.map_comp, Category.assoc] at eq

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
rw : liftAux hF α s (j.hom.unop ≫ i.f) = s.ι i ≫ R.map j.hom ≫ α.app j.right
⊢ (lift hF hR s ≫ R.map i.f.op) ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right

Tactic:
rw [Category.assoc, eq]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ j.hom.unop ≫ i.f = G.map (𝟙 (unop j.right)) ≫ j.hom.unop ≫ i.f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ liftAux hF α s (j.hom.unop ≫ i.f) = s.ι i ≫ R.map j.hom ≫ α.app j.right

Tactic:
simpa using liftAux_map hF α s (j.hom.unop ≫ i.f) (𝟙 _) i j.hom.unop (by simp)

Premises used: Quiver.Hom.unop, CategoryTheory.CategoryStruct.id, CategoryTheory.StructuredArrow.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.GrothendieckTopology.Cover.Arrow.f, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
apply :
  ∀ (j : StructuredArrow (op X) G.op),
    Eq (α := W ⟶ (StructuredArrow.proj (op X) G.op ⋙ F).obj j)
      (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j)
      (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j)
⊢ f = g

Tactic:
apply (hR (op X)).hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, Opposite.op