awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := unit S ⟶ (pushforward φ).obj (unit R))
    ((Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) (unit R) :
          (a : (pullback φ).obj (unit S) ⟶ unit R) → unit S ⟶ (pushforward φ).obj (unit R))
        (pullbackObjUnitToUnit φ) :
      unit S ⟶ (pushforward φ).obj (unit R))
    (unitToPushforwardObjUnit φ : unit S ⟶ (pushforward φ).obj (unit R))

Tactic:
Equiv.apply_symm_apply _ _

Premises used: Equiv.apply_symm_apply
-- 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
inst_6 : F.Final
rw :
  ∀ (T : SheafOfModules R),
    Function.Bijective (β := (pullback φ).obj (unit S) ⟶ T) fun (x : unit R ⟶ T) ↦ pullbackObjUnitToUnit φ ≫ x
⊢ IsIso (X := (pullback φ).obj (unit S)) (Y := unit R) (pullbackObjUnitToUnit φ)

Tactic:
rw [isIso_iff_coyoneda_map_bijective]

Premises used: CategoryTheory.isIso_iff_coyoneda_map_bijective
-- 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
inst_6 : F.Final
M : SheafOfModules R
rw :
  Function.Bijective (α := unit R ⟶ M) (β := ((pushforward φ).obj M).sections)
    (Function.comp (β := unit S ⟶ (pushforward φ).obj M)
      (⇑((pushforward φ).obj M).unitHomEquiv : (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
      (Function.comp (β := (pullback φ).obj (unit S) ⟶ M)
        (⇑(Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) M) :
          (a : (pullback φ).obj (unit S) ⟶ M) → unit S ⟶ (pushforward φ).obj M)
        fun (x : unit R ⟶ M) ↦ pullbackObjUnitToUnit φ ≫ x))
⊢ Function.Bijective (β := (pullback φ).obj (unit S) ⟶ M) fun (x : unit R ⟶ M) ↦ pullbackObjUnitToUnit φ ≫ x

Tactic:
rw [← ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).bijective.of_comp_iff',
    ← (unitHomEquiv _).bijective.of_comp_iff']

Premises used: SheafOfModules.unitHomEquiv, Equiv.bijective, Function.Bijective.of_comp_iff'
-- 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
inst_6 : F.Final
M : SheafOfModules R
⊢ Function.Bijective (α := unit R ⟶ M) (β := ((pushforward φ).obj M).sections)
    (pushforwardSections φ ∘ (⇑M.unitHomEquiv : (a : unit R ⟶ M) → M.sections))

Tactic:
(bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective

Premises used: SheafOfModules.unitHomEquiv, Equiv.bijective, SheafOfModules.bijective_pushforwardSections, Function.Bijective.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))
inst_5 : (pushforward φ).IsRightAdjoint
inst_6 : F.Final
M : SheafOfModules R
h :
  Eq (α := (unit R ⟶ M) → ((pushforward φ).obj M).sections)
    (Function.comp (β := unit S ⟶ (pushforward φ).obj M)
      (⇑((pushforward φ).obj M).unitHomEquiv : (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
      (Function.comp (β := (pullback φ).obj (unit S) ⟶ M)
        (⇑(Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) M) :
          (a : (pullback φ).obj (unit S) ⟶ M) → unit S ⟶ (pushforward φ).obj M)
        fun (x : unit R ⟶ M) ↦ pullbackObjUnitToUnit φ ≫ x))
    (pushforwardSections φ ∘ (⇑M.unitHomEquiv : (a : unit R ⟶ M) → M.sections))
⊢ Function.Bijective (α := unit R ⟶ M) (β := ((pushforward φ).obj M).sections)
    (Function.comp (β := unit S ⟶ (pushforward φ).obj M)
      (⇑((pushforward φ).obj M).unitHomEquiv : (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
      (Function.comp (β := (pullback φ).obj (unit S) ⟶ M)
        (⇑(Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) M) :
          (a : (pullback φ).obj (unit S) ⟶ M) → unit S ⟶ (pushforward φ).obj M)
        fun (x : unit R ⟶ M) ↦ pullbackObjUnitToUnit φ ≫ x))

Tactic:
convert! (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective

Premises used: SheafOfModules.unitHomEquiv, Equiv.bijective, SheafOfModules.bijective_pushforwardSections, Function.Bijective.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))
inst_5 : (pushforward φ).IsRightAdjoint
inst_6 : F.Final
M : SheafOfModules R
h :
  ∀ (f : unit R ⟶ M),
    Eq (α := ((pushforward φ).obj M).sections)
      (Function.comp (β := unit S ⟶ (pushforward φ).obj M)
        (⇑((pushforward φ).obj M).unitHomEquiv :
          (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
        (Function.comp (β := (pullback φ).obj (unit S) ⟶ M)
          (⇑(Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) M) :
            (a : (pullback φ).obj (unit S) ⟶ M) → unit S ⟶ (pushforward φ).obj M)
          fun (x : unit R ⟶ M) ↦ pullbackObjUnitToUnit φ ≫ x)
        f)
      ((pushforwardSections φ ∘ (⇑M.unitHomEquiv : (a : unit R ⟶ M) → M.sections)) f)
⊢ Eq (α := (unit R ⟶ M) → ((pushforward φ).obj M).sections)
    (Function.comp (β := unit S ⟶ (pushforward φ).obj M)
      (⇑((pushforward φ).obj M).unitHomEquiv : (a : unit S ⟶ (pushforward φ).obj M) → ((pushforward φ).obj M).sections)
      (Function.comp (β := (pullback φ).obj (unit S) ⟶ M)
        (⇑(Adjunction.homEquiv (pullbackPushforwardAdjunction φ) (unit S) M) :
          (a : (pullback φ).obj (unit S) ⟶ M) → unit S ⟶ (pushforward φ).obj M)
        fun (x : unit R ⟶ M) ↦ pullbackObjUnitToUnit φ ≫ x))
    (pushforwardSections φ ∘ (⇑M.unitHomEquiv : (a : unit R ⟶ M) → M.sections))

Tactic:
ext f : 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
inst_6 : HasWeakSheafify J AddCommGrpCat
inst_7 : HasWeakSheafify K AddCommGrpCat
inst_8 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_9 :
  K.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_10 : F.Final
I : Type u
i : I
⊢ Eq (α := (pullback φ).obj (unit S) ⟶ free I)
    (CategoryStruct.comp (Y := (pullback φ).obj (free I)) ((pullback φ).map (ιFree i))
      (Iso.hom (pullbackObjFreeIso φ I)))
    (pullbackObjUnitToUnit φ ≫ ιFree i)

Tactic:
simp [pullbackObjFreeIso, ιFree]

Premises used: SheafOfModules.pullbackObjFreeIso, SheafOfModules.ιFree
-- 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_1 : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J_1 RingCat
R : Sheaf K RingCat
inst_2 : F.IsContinuous J_1 K
φ : S ⟶ Functor.obj (F.sheafPushforwardContinuous RingCat J_1 K) R
inst_3 :
  J_1.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
inst_6 : HasWeakSheafify J_1 AddCommGrpCat
inst_7 : HasWeakSheafify K AddCommGrpCat
inst_8 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_9 :
  K.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_10 : F.Final
I J : Type u
f : I → J
i : I
⊢ Eq (α := (pullback φ).obj (unit S) ⟶ free J)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete I) (F := Discrete.functor fun (j : I) ↦ (pullback φ).obj (unit S))
          (Cofan.mk ((pullback φ).obj (free I)) fun (j : I) ↦ (pullback φ).map (ιFree j)))
        (Cofan.inj (f := fun (j : I) ↦ (pullback φ).obj (unit S))
          (Cofan.mk ((pullback φ).obj (free I)) fun (j : I) ↦ (pullback φ).map (ιFree j)) i)
        ((pullback φ).map (freeMap f) ≫ Iso.hom (pullbackObjFreeIso φ J)) :
      (pullback φ).obj (unit S) ⟶ free J)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete I) (F := Discrete.functor fun (j : I) ↦ (pullback φ).obj (unit S))
          (Cofan.mk ((pullback φ).obj (free I)) fun (j : I) ↦ (pullback φ).map (ιFree j)))
        (Cofan.inj (f := fun (j : I) ↦ (pullback φ).obj (unit S))
          (Cofan.mk ((pullback φ).obj (free I)) fun (j : I) ↦ (pullback φ).map (ιFree j)) i)
        (Iso.hom (pullbackObjFreeIso φ I) ≫ freeMap f) :
      (pullback φ).obj (unit S) ⟶ free J)

Tactic:
simp [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
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
φ_1 φ ψ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
e : φ = ψ
X : SheafOfModules.{v, v₂, u₂, u} R
U : Cᵒᵖ
subst : RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (φ.hom.app U)
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (ψ.hom.app U)

Tactic:
subst e
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
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
φ_1 φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
X : SheafOfModules.{v, v₂, u₂, u} R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (φ.hom.app U)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
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
φ_1 φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
X : SheafOfModules.{v, v₂, u₂, u} R
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
⊢ ((forget S).obj ((pushforward φ).obj X)).map x_2 ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf J).map x_2))).map
        (Iso.hom
          ((fun (U : Cᵒᵖ) ↦
              ((ModuleCat.restrictScalarsCongr ⋯).app
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) :
                (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                    ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) ≅
                  (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                    ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U)))
            x_1)) =
    Iso.hom
        ((fun (U : Cᵒᵖ) ↦
            ((ModuleCat.restrictScalarsCongr ⋯).app
                ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) :
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) ≅
                (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U)))
          x) ≫
      ((forget S).obj ((pushforward φ).obj X)).map x_2

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
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
φ_1 φ ψ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
e : φ = ψ
X Y : SheafOfModules.{v, v₂, u₂, u} R
x : X ⟶ Y
subst :
  (pushforward φ).map x ≫
      Iso.hom
        ((fun (X : SheafOfModules.{v, v₂, u₂, u} R) ↦
            ((fullyFaithfulForget S).preimageIso
                (PresheafOfModules.isoMk
                  (fun (U : Cᵒᵖ) ↦
                    (ModuleCat.restrictScalarsCongr ⋯).app
                      ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U))
                  ⋯) :
              (pushforward φ).obj X ≅ (pushforward φ).obj X))
          Y) =
    Iso.hom
        ((fun (X : SheafOfModules.{v, v₂, u₂, u} R) ↦
            ((fullyFaithfulForget S).preimageIso
                (PresheafOfModules.isoMk
                  (fun (U : Cᵒᵖ) ↦
                    (ModuleCat.restrictScalarsCongr ⋯).app
                      ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U))
                  ⋯) :
              (pushforward φ).obj X ≅ (pushforward φ).obj X))
          X) ≫
      (pushforward φ).map x
⊢ (pushforward φ).map x ≫
      Iso.hom
        ((fun (X : SheafOfModules.{v, v₂, u₂, u} R) ↦
            ((fullyFaithfulForget S).preimageIso
                (PresheafOfModules.isoMk
                  (fun (U : Cᵒᵖ) ↦
                    (ModuleCat.restrictScalarsCongr ⋯).app
                      ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U))
                  ⋯) :
              (pushforward φ).obj X ≅ (pushforward ψ).obj X))
          Y) =
    Iso.hom
        ((fun (X : SheafOfModules.{v, v₂, u₂, u} R) ↦
            ((fullyFaithfulForget S).preimageIso
                (PresheafOfModules.isoMk
                  (fun (U : Cᵒᵖ) ↦
                    (ModuleCat.restrictScalarsCongr ⋯).app
                      ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U))
                  ⋯) :
              (pushforward φ).obj X ≅ (pushforward ψ).obj X))
          X) ≫
      (pushforward ψ).map x

Tactic:
subst e
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
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
φ_1 φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
X Y : SheafOfModules.{v, v₂, u₂, u} R
x : X ⟶ Y
⊢ (pushforward φ).map x ≫
      Iso.hom
        ((fun (X : SheafOfModules.{v, v₂, u₂, u} R) ↦
            ((fullyFaithfulForget S).preimageIso
                (PresheafOfModules.isoMk
                  (fun (U : Cᵒᵖ) ↦
                    (ModuleCat.restrictScalarsCongr ⋯).app
                      ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U))
                  ⋯) :
              (pushforward φ).obj X ≅ (pushforward φ).obj X))
          Y) =
    Iso.hom
        ((fun (X : SheafOfModules.{v, v₂, u₂, u} R) ↦
            ((fullyFaithfulForget S).preimageIso
                (PresheafOfModules.isoMk
                  (fun (U : Cᵒᵖ) ↦
                    (ModuleCat.restrictScalarsCongr ⋯).app
                      ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U))
                  ⋯) :
              (pushforward φ).obj X ≅ (pushforward φ).obj X))
          X) ≫
      (pushforward φ).map x

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
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
e : φ = ψ
⊢ (pushforwardCongr e).symm = pushforwardCongr ⋯

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, SheafOfModules.pushforwardCongr, rfl, CategoryTheory.NatIso.ofComponents