awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
⊢ J.PreservesSheafification F
have mpr : J.W ≤ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
have hf₁ : IsIso (G₁.map f)
Tactic: rw [J.W_iff_isIso_map_of_adjunction adj₁] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight f F)
have mpr : J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)
Tactic: rw [← (W _).postcomp_iff _ _ (h P₂), ← whiskerRight_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)
have mpr : J.W (whiskerRight (adj₁.unit.app P₁ ≫ (G₁ ⋙ sheafToPresheaf J A).map f) F)
Tactic: erw [adj₁.unit.naturality f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (adj₁.unit.app P₁ ≫ (G₁ ⋙ sheafToPresheaf J A).map f) F)
have mpr : J.W (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
  (whiskerRight (adj₁.unit.app P₁ ≫ map (sheafToPresheaf J A) (G₁.map f)) F)
Tactic: dsimp only [Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
    (whiskerRight (adj₁.unit.app P₁ ≫ map (sheafToPresheaf J A) (G₁.map f)) F)
have mpr : J.W (X := (G₁ ⋙ sheafToPresheaf J A).obj P₁ ⋙ F) (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
  (whiskerRight (map (sheafToPresheaf J A) (G₁.map f)) F :
    (G₁ ⋙ sheafToPresheaf J A).obj P₁ ⋙ F ⟶ (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
Tactic: rw [whiskerRight_comp, (W _).precomp_iff _ _ (h P₁)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
⊢ Eq (α := (obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).obj P ⟶ (G₁ ⋙ sheafCompose J F).obj Q)
    ((obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).map f ≫
      (Equiv.symm (adj₂.homEquiv (obj (obj (whiskeringRight Cᵒᵖ A B) F) Q) ((G₁ ⋙ sheafCompose J F).obj Q)) :
          (a : ((whiskeringRight Cᵒᵖ A B).obj F).obj Q ⟶ (sheafToPresheaf J B).obj ((G₁ ⋙ sheafCompose J F).obj Q)) →
            G₂.obj (((whiskeringRight Cᵒᵖ A B).obj F).obj Q) ⟶ (G₁ ⋙ sheafCompose J F).obj Q)
        (whiskerRight (adj₁.unit.app Q) F))
    ((Equiv.symm (adj₂.homEquiv (obj (obj (whiskeringRight Cᵒᵖ A B) F) P) ((G₁ ⋙ sheafCompose J F).obj P)) :
          (a : ((whiskeringRight Cᵒᵖ A B).obj F).obj P ⟶ (sheafToPresheaf J B).obj ((G₁ ⋙ sheafCompose J F).obj P)) →
            G₂.obj (((whiskeringRight Cᵒᵖ A B).obj F).obj P) ⟶ (G₁ ⋙ sheafCompose J F).obj P)
        (whiskerRight (adj₁.unit.app P) F) ≫
      (G₁ ⋙ sheafCompose J F).map f)
have dsimp : Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
  (G₂.map (whiskerRight f F) ≫
    ((Equiv.symm (adj₂.homEquiv (Q ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (Q ⋙ F ⟶ (G₁.obj Q).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
            (G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))) :
        (a : Q ⋙ F ⟶ (G₁.obj Q).obj ⋙ F) → G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
      (whiskerRight (adj₁.unit.app Q) F))
  (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
          (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
            (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
        (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
      (whiskerRight (adj₁.unit.app P) F) ≫
    (sheafCompose J F).map (G₁.map f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
⊢ Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    (G₂.map (whiskerRight f F) ≫
      ((Equiv.symm (adj₂.homEquiv (Q ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
            (Q ⋙ F ⟶ (G₁.obj Q).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))) :
          (a : Q ⋙ F ⟶ (G₁.obj Q).obj ⋙ F) → G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight (adj₁.unit.app Q) F))
    (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
            (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
          (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
        (whiskerRight (adj₁.unit.app P) F) ≫
      (sheafCompose J F).map (G₁.map f))
have erw : Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
  ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
        (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
          G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
      (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) :
    G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
  ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
        (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
          G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
      (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) :
    G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
Tactic: erw [← adj₂.homEquiv_naturality_left_symm,
      ← adj₂.homEquiv_naturality_right_symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
⊢ Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
            G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) :
      G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
            G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) :
      G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
have h : whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F =
  whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
⊢ whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F =
    whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))
have h : ∀ (X : Cᵒᵖ),
  (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F).app X =
    NatTrans.app (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
X : Cᵒᵖ
⊢ (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F).app X =
    NatTrans.app (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) X
have this : (map (𝟭 (Functor.{v, v_1, u, u_1} Cᵒᵖ A)) f ≫ adj₁.unit.app Q).app X =
  (adj₁.unit.app P ≫ (G₁ ⋙ sheafToPresheaf J A).map f).app X
Tactic: have := NatTrans.congr_app (adj₁.unit.naturality f) X
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
X : Cᵒᵖ
this :
  (map (𝟭 (Functor.{v, v_1, u, u_1} Cᵒᵖ A)) f ≫ adj₁.unit.app Q).app X =
    (adj₁.unit.app P ≫ (G₁ ⋙ sheafToPresheaf J A).map f).app X
⊢ (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F).app X =
    NatTrans.app (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) X
have h : F.map (f.app X) ≫ F.map ((adj₁.unit.app Q).app X) = F.map ((adj₁.unit.app P).app X) ≫ F.map ((G₁.map f).hom.app X)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
⊢ α = NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P
have a : Eq (α := P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
  ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
          P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
      α :
    P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
  ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
          P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
      (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P) :
    P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
Tactic: apply (adj₂.homEquiv _ _).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
⊢ Eq (α := P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
            P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
        α :
      P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
            P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
        (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P) :
      P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
have a : Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
  ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
      α :
    P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
  ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
      (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
            (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
          (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
        (whiskerRight (adj₁.unit.app P) F)) :
    P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
Tactic: dsimp [sheafComposeNatTrans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
⊢ Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        α :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
              (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
                (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
            (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
          (whiskerRight (adj₁.unit.app P) F)) :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
have a : (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
      (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
    α =
  whiskerRight (adj₁.unit.app P) F
Tactic: erw [Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
      α =
    whiskerRight (adj₁.unit.app P) F
have a : Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
  ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
      α :
    P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
  (adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α :
    obj (𝟭 (Functor.{v, v_2, u, u_2} Cᵒᵖ B)) (P ⋙ F) ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
Tactic: rw [← hα]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
⊢ J.PreservesSheafification F ↔ IsIso (Y := G₁ ⋙ sheafCompose J F) (sheafComposeNatTrans J F adj₁ adj₂)
have rw : (∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
  ∀ (X : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
    IsIso (Y := (G₁ ⋙ sheafCompose J F).obj X) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) X)
Tactic: rw [J.preservesSheafification_iff_of_adjunctions F adj₁ adj₂,
    NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
⊢ (∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
      IsIso (Y := (G₁ ⋙ sheafCompose J F).obj X) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) X)
have h : ∀ (a : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
  IsIso (G₂.map (whiskerRight (adj₁.unit.app a) F)) ↔
    IsIso (Y := (G₁ ⋙ sheafCompose J F).obj a) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) a)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F)) ↔
    IsIso (Y := (G₁ ⋙ sheafCompose J F).obj P) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P)
have h : J.W (whiskerRight (adj₁.unit.app P) F) ↔
  IsIso (Y := (G₁ ⋙ sheafCompose J F).obj P) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P)
Tactic: rw [← J.W_iff_isIso_map_of_adjunction adj₂, ← J.W_sheafToPresheaf_map_iff_isIso,
    ← sheafComposeNatTrans_fac J F adj₁ adj₂,
    (W _).precomp_iff _ _ (J.W_adj_unit_app adj₂ (P ⋙ F))]