awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).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_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
inst_4 : M.IsFinitePresentation
obtain : ∀ (σ : M.QuasicoherentData), σ.IsFinitePresentation → ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType
⊢ ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType

Tactic:
obtain ⟨σ, _⟩ := IsFinitePresentation.exists_quasicoherentData M

Premises used: SheafOfModules.IsFinitePresentation.exists_quasicoherentData
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).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_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
inst_4 : M.IsFinitePresentation
σ : M.QuasicoherentData
h : σ.IsFinitePresentation
⊢ ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType

Tactic:
⟨σ.localGeneratorsData, inferInstance⟩

Premises used: inferInstance, Exists.intro, SheafOfModules.QuasicoherentData.localGeneratorsData
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).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_2 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
inst_4 : M.IsFinitePresentation
σ : M.QuasicoherentData
h : σ.IsFinitePresentation
⊢ ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType

Tactic:
exact ⟨σ.localGeneratorsData, inferInstance⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_5 :
  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_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
P : M.Presentation
x : C
rw : ∀ ⦃Y : C⦄ (f : Y ⟶ x), Sieve.arrows (Sieve.ofObjects id x) f ↔ Sieve.arrows ⊤ f
⊢ Eq (α := Sieve.{v₁, u₁} x) (Sieve.ofObjects id x) ⊤

Tactic:
rw [Sieve.ext_iff]

Premises used: CategoryTheory.Sieve.ext_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_5 :
  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_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
P : M.Presentation
x Y : C
f : Y ⟶ x
⊢ Sieve.arrows (Sieve.ofObjects id x) f ↔ Sieve.arrows ⊤ f

Tactic:
simpa [Sieve.top_apply, iff_true] using ⟨x, Nonempty.intro f⟩

Premises used: CategoryTheory.Sieve.top_apply, iff_true
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_5 :
  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_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M : SheafOfModules R
P : M.Presentation
x : C
⊢ unit (R.over x) ≅ unit (R.over x)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.464457}) ↦
    (↑x1 : Type ?u.464457) →+ (↑x2 : Type ?u.464457)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.465971}) ↦ (↑R : Type ?u.465971) →+* (↑S : Type ?u.465971)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.465971}) ↦
      (↑x1 : Type ?u.465971) →+ (↑x2 : Type ?u.465971)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
X Y : SheafOfModules R
e : X ≅ Y
q : X.QuasicoherentData
⊢ isQuasicoherent R Y

Tactic:
⟨⟨q.ofIsIso e.hom⟩⟩

Premises used: Nonempty.intro, SheafOfModules.IsQuasicoherent.mk, CategoryTheory.Iso.hom, SheafOfModules.QuasicoherentData.ofIsIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.464457}) ↦
    (↑x1 : Type ?u.464457) →+ (↑x2 : Type ?u.464457)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.465971}) ↦ (↑R : Type ?u.465971) →+* (↑S : Type ?u.465971)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.465971}) ↦
      (↑x1 : Type ?u.465971) →+ (↑x2 : Type ?u.465971)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
X Y : SheafOfModules R
e : X ≅ Y
q : X.QuasicoherentData
⊢ isQuasicoherent R Y

Tactic:
exact ⟨⟨q.ofIsIso e.hom⟩⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.475740}) ↦
    (↑x1 : Type ?u.475740) →+ (↑x2 : Type ?u.475740)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.477254}) ↦ (↑R : Type ?u.477254) →+* (↑S : Type ?u.477254)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.477254}) ↦
      (↑x1 : Type ?u.477254) →+ (↑x2 : Type ?u.477254)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M N : SheafOfModules R
f : M ⟶ N
inst_9 : IsIso f
σ : QuasicoherentData.{u_1, u, v₁, u₁} M
inst_10 : σ.IsFinitePresentation
i : QuasicoherentData.I (QuasicoherentData.ofIsIso f σ : QuasicoherentData.{u_1, u, v₁, u₁} N)
dsimp :
  Presentation.IsFinite
    (Presentation.ofIsIso (Hom.over f (σ.X i)) (σ.presentation i) :
      Presentation (C := Over.{v₁, u₁} (σ.X i)) (N.over (σ.X i)))
⊢ Presentation.IsFinite (C := Over.{v₁, u₁} (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i)) (J :=
    (J.over (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i) :
      GrothendieckTopology (Over.{v₁, u₁} (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i))))
    (R :=
    (R.over (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i) :
      Sheaf (C := Over.{v₁, u₁} (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i))
        (J.over (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i)) RingCat))
    (M :=
    (N.over (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i) :
      SheafOfModules (C := Over.{v₁, u₁} (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i))
        (R.over (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i))))
    (QuasicoherentData.presentation (QuasicoherentData.ofIsIso f σ) i :
      Presentation (C := Over.{v₁, u₁} (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i))
        (N.over (QuasicoherentData.X (QuasicoherentData.ofIsIso f σ) i)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.475740}) ↦
    (↑x1 : Type ?u.475740) →+ (↑x2 : Type ?u.475740)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.477254}) ↦ (↑R : Type ?u.477254) →+* (↑S : Type ?u.477254)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.477254}) ↦
      (↑x1 : Type ?u.477254) →+ (↑x2 : Type ?u.477254)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M N : SheafOfModules R
f : M ⟶ N
inst_9 : IsIso f
σ : QuasicoherentData.{u_1, u, v₁, u₁} M
inst_10 : σ.IsFinitePresentation
i : QuasicoherentData.I (QuasicoherentData.ofIsIso f σ : QuasicoherentData.{u_1, u, v₁, u₁} N)
⊢ Presentation.IsFinite
    (Presentation.ofIsIso (Hom.over f (σ.X i)) (σ.presentation i) :
      Presentation (C := Over.{v₁, u₁} (σ.X i)) (N.over (σ.X i)))

Tactic:
inferInstanceAs ((σ.presentation i).ofIsIso _).IsFinite

Premises used: _private.0.SheafOfModules.instIsFinitePresentationOfIsIso._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.475740}) ↦
    (↑x1 : Type ?u.475740) →+ (↑x2 : Type ?u.475740)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.477254}) ↦ (↑R : Type ?u.477254) →+* (↑S : Type ?u.477254)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.477254}) ↦
      (↑x1 : Type ?u.477254) →+ (↑x2 : Type ?u.477254)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
M N : SheafOfModules R
f : M ⟶ N
inst_9 : IsIso f
σ : QuasicoherentData.{u_1, u, v₁, u₁} M
inst_10 : σ.IsFinitePresentation
i : QuasicoherentData.I (QuasicoherentData.ofIsIso f σ : QuasicoherentData.{u_1, u, v₁, u₁} N)
⊢ Presentation.IsFinite
    (Presentation.ofIsIso (Hom.over f (σ.X i)) (σ.presentation i) :
      Presentation (C := Over.{v₁, u₁} (σ.X i)) (N.over (σ.X i)))

Tactic:
exact inferInstanceAs ((σ.presentation i).ofIsIso _).IsFinite
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.487206}) ↦
    (↑x1 : Type ?u.487206) →+ (↑x2 : Type ?u.487206)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.488720}) ↦ (↑R : Type ?u.488720) →+* (↑S : Type ?u.488720)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.488720}) ↦
      (↑x1 : Type ?u.488720) →+ (↑x2 : Type ?u.488720)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
X Y : SheafOfModules R
e : X ≅ Y
σ : X.QuasicoherentData
hσ : σ.IsFinitePresentation
⊢ isFinitePresentation R Y

Tactic:
⟨σ.ofIsIso e.hom, inferInstance⟩

Premises used: SheafOfModules.IsFinitePresentation.mk, inferInstance, Exists.intro, CategoryTheory.Iso.hom, SheafOfModules.QuasicoherentData.ofIsIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : HasBinaryProducts.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_3 : HasSheafify J AddCommGrpCat
inst_4 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{?u.487206}) ↦
    (↑x1 : Type ?u.487206) →+ (↑x2 : Type ?u.487206)) (CA := AddCommGrpCat.carrier)
inst_5 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{?u.488720}) ↦ (↑R : Type ?u.488720) →+* (↑S : Type ?u.488720)) (CC :=
      RingCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{?u.488720}) ↦
      (↑x1 : Type ?u.488720) →+ (↑x2 : Type ?u.488720)) (CD := AddCommGrpCat.carrier))
inst_6 :
  ∀ (X : C),
    (J.over X).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_7 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_8 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
X Y : SheafOfModules R
e : X ≅ Y
σ : X.QuasicoherentData
hσ : σ.IsFinitePresentation
⊢ isFinitePresentation R Y

Tactic:
exact ⟨σ.ofIsIso e.hom, inferInstance⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R_1 : Sheaf J RingCat
inst_1 :
  ∀ (X : C),
    (J.over X).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_2 : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst_3 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
inst_4 :
  ∀ (X : C) (Y : Over.{v₁, u₁} X),
    ((J.over X).over Y).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 : ∀ (X : C) (Y : Over.{v₁, u₁} X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst_6 :
  ∀ (X : C) (Y : Over.{v₁, u₁} X),
    ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := AddCommGrpCat.carrier)
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → QuasicoherentData (C := Over.{v₁, u₁} (X i)) (M.over (X i))
i : (i : I) × (D i).I
x :
  (Over.{v₁, u₁}
      (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I))) (i.snd (β := fun (i : I) ↦ (D i).I))).left)ᵒᵖ
⊢ (Functor.whiskerRight
          (NatTrans.op
            (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I)))
                  (i.snd (β := fun (i : I) ↦ (D i).I))).iteratedSliceEquiv.counit)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf
              (J.over
                (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I)))
                    (i.snd (β := fun (i : I) ↦ (D i).I))).left))
            (R.over
              (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I)))
                  (i.snd (β := fun (i : I) ↦ (D i).I))).left))).app
      x =
    NatTrans.app
      (InducedCategory.Hom.hom
          (𝟙
            (R.over
              (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I)))
                  (i.snd (β := fun (i : I) ↦ (D i).I))).left)) ≫
        (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I)))
                    (i.snd (β := fun (i : I) ↦ (D i).I))).iteratedSliceEquiv.inverse.op.whiskerLeft
          (InducedCategory.Hom.hom
            (𝟙
              (Sheaf.over (R.over (X (i.fst (β := fun (i : I) ↦ (D i).I))))
                (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I))) (i.snd (β := fun (i : I) ↦ (D i).I)))))))
      x

Tactic:
R.1.map_id _

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_id