awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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 a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
have 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))
Tactic: simp only [Functor.map_comp, Functor.map_id, Category.id_comp] at eq₁ eq₂
Cleared hypotheses: eq₁, eq₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ lift hF hR s ≫ R.map i.f.op = s.ι i
have 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)
Tactic: apply (hR (op i.Y)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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 ⟶ (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)
have 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)))))
Tactic: have eq := fac' hF hR s (StructuredArrow.mk (i.f.op ≫ j.hom))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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)))))
⊢ 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)
have 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
Tactic: dsimp at eq ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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 = s.ι i ≫ R.map j.hom ≫ α.app j.right
have 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)
Tactic: simp only [Functor.map_comp, Category.assoc] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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)
⊢ (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
have rw : liftAux hF α s (j.hom.unop ≫ i.f) = s.ι i ≫ R.map j.hom ≫ α.app j.right
Tactic: rw [Category.assoc, eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ f = g
have 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)
Tactic: apply (hR (op X)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
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)
have h₁ : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
        Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
        (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) sorry)),
  (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫ F.map I.f.op =
    (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫ F.map I.f.op
Tactic: apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
⊢ (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫
      F.map
        { Y := W, f := i, hf := hi :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
                  Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right)))
                    ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
                  (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) }.f.op =
    (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫
      F.map
        { Y := W, f := i, hf := hi :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
                  Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right)))
                    ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
                  (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) }.f.op
have eq : f ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi : S.Arrow }.f.op =
  g ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op
Tactic: have eq := h (GrothendieckTopology.Cover.Arrow.mk _ (G.map i ≫ j.hom.unop) hi)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
eq :
  f ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi : S.Arrow }.f.op =
    g ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op
⊢ (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫
      F.map
        { Y := W, f := i, hf := hi :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
                  Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right)))
                    ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
                  (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) }.f.op =
    (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫
      F.map
        { Y := W, f := i, hf := hi :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
                  Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right)))
                    ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
                  (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) }.f.op
have h₁ : (f ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op
Tactic: dsimp at eq ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
⊢ (f ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op
have h₁ : f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
Tactic: simp only [Category.assoc, ← NatTrans.naturality, Functor.comp_map, ← Functor.map_comp_assoc,
    Functor.op_map, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
⊢ f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
have h₁ : g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
Tactic: rw [reassoc_of% eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf.{v_1, w', u_1, w} J A
⊢ Presheaf.IsSheaf K (Functor.obj G.op.ran (ℱ.obj (P := Presheaf.IsSheaf J)))
have rw : ∀ (X : D) (S : K.Cover X), Nonempty (IsLimit (S.multifork (Functor.obj G.op.ran (ℱ.obj (P := Presheaf.IsSheaf J)))))
Tactic: rw [Presheaf.isSheaf_iff_multifork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
⊢ Eq (α :=
    (obj (𝟭 (Sheaf.{v_2, w', u_2, w} K A)) F).obj (P := Presheaf.IsSheaf K) ⟶
      (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K) F).obj (P := Presheaf.IsSheaf K))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.unit (G.sheafAdjunctionCocontinuous A J K)) F))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))
have apply : Eq (α :=
  obj (sheafToPresheaf K A) (obj (𝟭 (Sheaf.{v_2, w', u_2, w} K A)) F) ⟶
    obj (sheafToPresheaf K A) (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K) F))
  (CategoryStruct.comp (Y := obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (obj (sheafToPresheaf K A) F))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (obj (sheafToPresheaf K A) F))
    (map G.op.ran (NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K))) F) ≫
      NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K)))
        (obj (G.sheafPushforwardContinuous A J K) F)))
  (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))
Tactic: apply ((G.op.ranAdjunction A).map_restrictFullyFaithful_unit_app
    (fullyFaithfulSheafToPresheaf K A) (fullyFaithfulSheafToPresheaf J A)
    (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
    (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm F).trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
⊢ Eq (α :=
    obj (sheafToPresheaf K A) (obj (𝟭 (Sheaf.{v_2, w', u_2, w} K A)) F) ⟶
      obj (sheafToPresheaf K A) (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K) F))
    (CategoryStruct.comp (Y := obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (obj (sheafToPresheaf K A) F))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (obj (sheafToPresheaf K A) F))
      (map G.op.ran (NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K))) F) ≫
        NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K)))
          (obj (G.sheafPushforwardContinuous A J K) F)))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))
have dsimp : Eq (α :=
  F.obj (P := Presheaf.IsSheaf K) ⟶
    (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
      Presheaf.IsSheaf K))
  (CategoryStruct.comp (Y := obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) :
      obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) (F.obj (P := Presheaf.IsSheaf K)) ⟶
        obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (F.obj (P := Presheaf.IsSheaf K)))
    (CategoryStruct.comp (Y :=
      obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
      (map G.op.ran (NatTrans.app (Iso.inv (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K)) F) :
        obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)) ⟶
          obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
      (𝟙
          ((obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
            Presheaf.IsSheaf K)) :
        (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
            Presheaf.IsSheaf K) ⟶
          (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
            Presheaf.IsSheaf K))))
  (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))
Tactic: dsimp