awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R₀ : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_4 : HasWeakSheafify J AddCommGrpCat
⊢ (sheafification α).IsLocalization
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α))

Tactic:
(sheafificationAdjunction.{v} α).isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization, PresheafOfModules.sheafificationAdjunction
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R₀ : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj (P := Presheaf.IsSheaf J)
inst_1 :
  Presheaf.IsLocallyInjective (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier)
    J α
inst_2 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_4 : HasWeakSheafify J AddCommGrpCat
⊢ (sheafification α).IsLocalization
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α))

Tactic:
exact (sheafificationAdjunction.{v} α).isLocalization
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_5 : (pushforward φ).IsRightAdjoint
⊢ (pullback φ).IsLeftAdjoint

Tactic:
(pullbackPushforwardAdjunction φ).isLeftAdjoint

Premises used: SheafOfModules.pullbackPushforwardAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_5 : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst_6 : HasWeakSheafify K AddCommGrpCat
inst_7 :
  K.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
X' X : SheafOfModules.{v, v₁, u₁, u} S
Y : SheafOfModules.{v, v₂, u₂, u} R
f : X' ⟶ X
g : X ⟶ (pushforward φ).obj Y
⊢ Eq (α :=
    (PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
        ((PresheafOfModules.pullback φ.hom).obj X'.val) ⟶
      Y)
    ((PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).map
        ((PresheafOfModules.pullback φ.hom).map (f.val ≫ g.val)) ≫
      (Equiv.symm
            (Adjunction.homEquiv (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf K))))
              ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y.val)) Y) :
          (a :
              (PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y.val) ⟶
                Y.val.restrictScalarsObj (𝟙 R.obj)) →
            (PresheafOfModules.sheafification (𝟙 R.obj)).obj
                ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y.val)) ⟶
              Y)
        (NatTrans.app (Adjunction.counit (PresheafOfModules.pullbackPushforwardAdjunction φ.hom)) Y.val))
    ((PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).map
        ((PresheafOfModules.pullback φ.hom).map f.val) ≫
      (PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).map
          ((PresheafOfModules.pullback φ.hom).map g.val) ≫
        (Equiv.symm
              (Adjunction.homEquiv (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf K))))
                ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y.val)) Y) :
            (a :
                (PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y.val) ⟶
                  Y.val.restrictScalarsObj (𝟙 R.obj)) →
              (PresheafOfModules.sheafification (𝟙 R.obj)).obj
                  ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y.val)) ⟶
                Y)
          (NatTrans.app (Adjunction.counit (PresheafOfModules.pullbackPushforwardAdjunction φ.hom)) Y.val))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_5 : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst_6 : HasWeakSheafify K AddCommGrpCat
inst_7 :
  K.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
⊢ (pushforward φ).IsRightAdjoint

Tactic:
(PullbackConstruction.adjunction.{v} φ).isRightAdjoint

Premises used: SheafOfModules.PullbackConstruction.adjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
⊢ IsRightAdjoint (C := SheafOfModules.{v, v₁, u₁, u} S) (D := SheafOfModules.{v, v₁, u₁, u} S)
    (pushforward (F := 𝟭 C) (𝟙 S))

Tactic:
Functor.isRightAdjoint_of_iso (pushforwardId S).symm

Premises used: SheafOfModules.pushforwardId, CategoryTheory.Iso.symm, CategoryTheory.Functor.isRightAdjoint_of_iso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
S : Sheaf J RingCat
⊢ (conjugateEquiv Adjunction.id (pullbackPushforwardAdjunction (𝟙 S)) :
        (a : pullback (𝟙 S) ⟶ 𝟭 (SheafOfModules S)) → 𝟭 (SheafOfModules S) ⟶ pushforward (𝟙 S))
      (pullbackId S).hom =
    (pushforwardId S).inv

Tactic:
Adjunction.conjugateEquiv_leftAdjointIdIso_hom _ _

Premises used: CategoryTheory.Adjunction.conjugateEquiv_leftAdjointIdIso_hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_5 : (pushforward φ).IsRightAdjoint
K' : GrothendieckTopology.{v₃, u₃} D'
K'' : GrothendieckTopology.{v₄, u₄} D''
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_6 : G.IsContinuous K K'
inst_7 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
inst_8 : (pushforward ψ).IsRightAdjoint
⊢ (pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ)).IsRightAdjoint

Tactic:
Functor.isRightAdjoint_of_iso (pushforwardComp.{v} φ ψ)

Premises used: CategoryTheory.Functor.isRightAdjoint_of_iso, SheafOfModules.pushforwardComp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_3 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_4 : (pushforward φ).IsRightAdjoint
K' : GrothendieckTopology.{v₃, u₃} D'
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_5 : G.IsContinuous K K'
inst_6 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
inst_7 : (pushforward ψ).IsRightAdjoint
⊢ Eq (α :=
    pushforward ψ ⋙ pushforward φ ⟶
      pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ))
    ((conjugateEquiv (Adjunction.comp (pullbackPushforwardAdjunction φ) (pullbackPushforwardAdjunction ψ))
            (pullbackPushforwardAdjunction
              (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ)) :
          (a : pullback (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ⟶ pullback φ ⋙ pullback ψ) →
            pushforward ψ ⋙ pushforward φ ⟶ pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ))
        (Iso.inv (pullbackComp φ ψ)) :
      pushforward ψ ⋙ pushforward φ ⟶
        pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ))
    (Iso.hom (pushforwardComp φ ψ) :
      pushforward ψ ⋙ pushforward φ ⟶
        pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ))

Tactic:
Adjunction.conjugateEquiv_leftAdjointCompIso_inv _ _ _ _

Premises used: CategoryTheory.Adjunction.conjugateEquiv_leftAdjointCompIso_inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_5 : (pushforward φ).IsRightAdjoint
K' : GrothendieckTopology.{v₃, u₃} D'
K'' : GrothendieckTopology.{v₄, u₄} D''
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_6 : G.IsContinuous K K'
inst_7 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
inst_8 : (pushforward ψ).IsRightAdjoint
G' : CategoryTheory.Functor.{v₃, v₄, u₃, u₄} D' D''
R'' : Sheaf K'' RingCat
inst_9 : G'.IsContinuous K' K''
inst_10 : (G ⋙ G').IsContinuous K K''
inst_11 : ((F ⋙ G) ⋙ G').IsContinuous J K''
inst_12 : (F ⋙ G ⋙ G').IsContinuous J K''
ψ' : R' ⟶ obj (G'.sheafPushforwardContinuous RingCat K' K'') R''
inst_13 : (pushforward ψ').IsRightAdjoint
⊢ Eq (α :=
    pullback φ ⋙ pullback ψ ⋙ pullback ψ' ≅
      pullback
        (φ ≫
          CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K)
            (ψ ≫ CategoryTheory.Functor.map (G.sheafPushforwardContinuous RingCat K K') ψ')))
    (Iso.trans (Y :=
      pullback φ ⋙ pullback (ψ ≫ CategoryTheory.Functor.map (G.sheafPushforwardContinuous RingCat K K') ψ'))
      ((pullback φ).isoWhiskerLeft (pullbackComp ψ ψ'))
      (pullbackComp φ (ψ ≫ CategoryTheory.Functor.map (G.sheafPushforwardContinuous RingCat K K') ψ')))
    (((pullback φ).associator (pullback ψ) (pullback ψ')).symm ≪≫
      Iso.trans (Y :=
        pullback (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ) ⋙ pullback ψ')
        (isoWhiskerRight (pullbackComp φ ψ) (pullback ψ'))
        (pullbackComp (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ) ψ'))

Tactic:
Adjunction.leftAdjointCompIso_assoc _ _ _ _ _ _ _ _ _ _ (pushforward_assoc φ ψ ψ')

Premises used: SheafOfModules.pushforward_assoc, CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.op, CategoryTheory.Functor.comp, SheafOfModules.pullbackComp, CategoryTheory.Adjunction.leftAdjointCompIso_assoc
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_3 : (pushforward φ).IsRightAdjoint
⊢ pullbackComp (𝟙 S) φ = isoWhiskerRight (pullbackId S) (pullback φ) ≪≫ (pullback φ).leftUnitor

Tactic:
Adjunction.leftAdjointCompIso_id_comp _ _ _ _ (pushforward_comp_id φ)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, SheafOfModules.pullbackComp, SheafOfModules.pullbackId, CategoryTheory.Adjunction.leftAdjointCompIso_id_comp, SheafOfModules.pushforward_comp_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_3 : (pushforward φ).IsRightAdjoint
⊢ pullbackComp φ (𝟙 R) = (pullback φ).isoWhiskerLeft (pullbackId R) ≪≫ (pullback φ).rightUnitor

Tactic:
Adjunction.leftAdjointCompIso_comp_id _ _ _ _ (pushforward_id_comp φ)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, SheafOfModules.pullbackComp, SheafOfModules.pullbackId, CategoryTheory.Adjunction.leftAdjointCompIso_comp_id, SheafOfModules.pushforward_id_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J K
φ : S ⟶ Functor.obj (F.sheafPushforwardContinuous RingCat J K) R
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
inst_4 :
  K.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
X : Cᵒᵖ
a : (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u)
⊢ Eq (α := (↑(((pushforward φ).obj (unit R)).val.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
            LinearMap (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (X := (unit S).val.obj X) (Y := ((pushforward φ).obj (unit R)).val.obj X)
            (PresheafOfModules.Hom.app (Hom.val (unitToPushforwardObjUnit φ)) X) :
          (a : (↑((unit S).val.obj X) : Type u)) → (↑(((pushforward φ).obj (unit R)).val.obj X) : Type u))
        a :
      (↑(((pushforward φ).obj (unit R)).val.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (φ.hom.app X) :
          (a : (↑(S.obj.obj X) : Type u)) → (↑(((F.sheafPushforwardContinuous RingCat J K).obj R).obj.obj X) : Type u))
        a :
      (↑((Functor.obj (F.sheafPushforwardContinuous RingCat J K) R).obj (P := Presheaf.IsSheaf J).obj X) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J K
φ : S ⟶ Functor.obj (F.sheafPushforwardContinuous RingCat J K) R
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
inst_4 :
  K.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
f : unit R ⟶ M
h :
  ∀ (X : Cᵒᵖ),
    Eq (α :=
      (((pushforward φ).obj M).val.presheaf ⋙
            CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).obj
        X)
      ((↑(pushforwardSections φ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) f)) :
            (j : Cᵒᵖ) → (((pushforward φ).obj M).val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
          X :
        (((pushforward φ).obj M).val.presheaf ⋙
              CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier)).obj
          X)
      ((↑((((pushforward φ).obj M).unitHomEquiv :
                  (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
                (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f)) :
            (j : Cᵒᵖ) → (((pushforward φ).obj M).val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
          X :
        (((pushforward φ).obj M).val.presheaf ⋙
              CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier)).obj
          X)
⊢ Eq (α := ((pushforward φ).obj M).sections)
    (pushforwardSections φ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) f))
    ((((pushforward φ).obj M).unitHomEquiv : (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
      (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f))

Tactic:
ext X
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J K
φ : S ⟶ Functor.obj (F.sheafPushforwardContinuous RingCat J K) R
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
inst_4 :
  K.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ Eq (α := (↑(((pushforward φ).obj (unit R)).val.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
            LinearMap (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (X := (unit S).val.obj X) (Y := ((pushforward φ).obj (unit R)).val.obj X)
            (PresheafOfModules.Hom.app (Hom.val (unitToPushforwardObjUnit φ)) X) :
          (a : (↑((unit S).val.obj X) : Type u)) → (↑(((pushforward φ).obj (unit R)).val.obj X) : Type u))
        1 :
      (↑(((pushforward φ).obj (unit R)).val.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (φ.hom.app X) :
          (a : (↑(S.obj.obj X) : Type u)) → (↑(((F.sheafPushforwardContinuous RingCat J K).obj R).obj.obj X) : Type u))
        1 :
      (↑((Functor.obj (F.sheafPushforwardContinuous RingCat J K) R).obj (P := Presheaf.IsSheaf J).obj X) : Type u))

Tactic:
have := unitToPushforwardObjUnit_val_app_apply φ (X := X) 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J K
φ : S ⟶ Functor.obj (F.sheafPushforwardContinuous RingCat J K) R
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
inst_4 :
  K.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
inst_5 : (pushforward φ).IsRightAdjoint
⊢ Eq (α := (pullback φ).obj (unit S) ⟶ unit R)
    ((Equiv.symm (Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) (unit R)) :
          (a : unit S ⟶ (pushforward φ).obj (unit R)) → (pullback φ).obj (unit S) ⟶ unit R)
        (unitToPushforwardObjUnit φ) :
      (pullback φ).obj (unit S) ⟶ unit R)
    (pullbackObjUnitToUnit φ : (pullback φ).obj (unit S) ⟶ unit R)

Tactic:
rfl

Premises used: SheafOfModules.pullbackObjUnitToUnit, rfl