awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F_1 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R_1 : Sheaf K_1 RingCat
inst_4 : F_1.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F_1.sheafPushforwardContinuous RingCat J_1 K_1) R_1
C_2 : Type u₁
inst_5 : Category.{v₁, u₁} C_2
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J_2 : GrothendieckTopology.{v₁, u₁} C_2
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_2 D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C_2
S : Sheaf J_2 RingCat
R_2 : Sheaf K RingCat
inst_7 : F.IsContinuous J_2 K
inst_8 : G.IsContinuous K J_2
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J_2 K) R_2
ψ : R_2 ⟶ obj (G.sheafPushforwardContinuous RingCat K J_2) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R_2.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J_2)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J_2))
C : Type u'
inst_9 : Category.{v', u'} C
inst_10 : HasBinaryProducts.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
x : C
⊢ pushforward (𝟙 (R.over x)) ⊣ pushforward (F := Over.star x) (pushforwardOver x)
have refine_1 : Eq (α :=
  Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J) ⟶
    Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J))
  (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J)))
  (InducedCategory.Hom.hom (pushforwardOver x) ≫
    whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
Tactic: refine pushforwardPushforwardAdj (Over.forgetAdjStar x) (𝟙 (R.over x)) _ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F_1 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R_1 : Sheaf K_1 RingCat
inst_4 : F_1.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F_1.sheafPushforwardContinuous RingCat J_1 K_1) R_1
C_2 : Type u₁
inst_5 : Category.{v₁, u₁} C_2
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J_2 : GrothendieckTopology.{v₁, u₁} C_2
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_2 D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C_2
S : Sheaf J_2 RingCat
R_2 : Sheaf K RingCat
inst_7 : F.IsContinuous J_2 K
inst_8 : G.IsContinuous K J_2
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J_2 K) R_2
ψ : R_2 ⟶ obj (G.sheafPushforwardContinuous RingCat K J_2) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R_2.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J_2)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J_2))
C : Type u'
inst_9 : Category.{v', u'} C
inst_10 : HasBinaryProducts.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
x : C
refine_1 :
  Eq (α :=
    Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J) ⟶
      Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J))
    (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J)))
    (InducedCategory.Hom.hom (pushforwardOver x) ≫
      whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
⊢ pushforward (𝟙 (R.over x)) ⊣ pushforward (F := Over.star x) (pushforwardOver x)
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine pushforwardPushforwardAdj (Over.forgetAdjStar x) (𝟙 (R.over x)) _ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F_1 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R_1 : Sheaf K_1 RingCat
inst_4 : F_1.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F_1.sheafPushforwardContinuous RingCat J_1 K_1) R_1
C_2 : Type u₁
inst_5 : Category.{v₁, u₁} C_2
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J_2 : GrothendieckTopology.{v₁, u₁} C_2
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_2 D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C_2
S : Sheaf J_2 RingCat
R_2 : Sheaf K RingCat
inst_7 : F.IsContinuous J_2 K
inst_8 : G.IsContinuous K J_2
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J_2 K) R_2
ψ : R_2 ⟶ obj (G.sheafPushforwardContinuous RingCat K J_2) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R_2.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J_2)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J_2))
C : Type u'
inst_9 : Category.{v', u'} C
inst_10 : HasBinaryProducts.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
x : C
⊢ Eq (α :=
    Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J) ⟶
      Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J))
    (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J)))
    (InducedCategory.Hom.hom (pushforwardOver x) ≫
      whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
have refine_1 : ∀ (y : Cᵒᵖ),
  Eq (α :=
    (Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J)).obj y ⟶
      (Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J)).obj y)
    (NatTrans.app
      (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J))) y)
    (NatTrans.app
      (InducedCategory.Hom.hom (pushforwardOver x) ≫
        whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
      y)
Tactic: ext y : 2
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F_1 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R_1 : Sheaf K_1 RingCat
inst_4 : F_1.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F_1.sheafPushforwardContinuous RingCat J_1 K_1) R_1
C_2 : Type u₁
inst_5 : Category.{v₁, u₁} C_2
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J_2 : GrothendieckTopology.{v₁, u₁} C_2
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_2 D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C_2
S : Sheaf J_2 RingCat
R_2 : Sheaf K RingCat
inst_7 : F.IsContinuous J_2 K
inst_8 : G.IsContinuous K J_2
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J_2 K) R_2
ψ : R_2 ⟶ obj (G.sheafPushforwardContinuous RingCat K J_2) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R_2.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J_2)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J_2))
C : Type u'
inst_9 : Category.{v', u'} C
inst_10 : HasBinaryProducts.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
x : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext y : 2
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R_1 : Sheaf K_1 RingCat
inst_4 : F.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F.sheafPushforwardContinuous RingCat J_1 K_1) R_1
C : Type u₁
inst_5 : Category.{v₁, u₁} C
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
eqv : CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : eqv.functor.IsContinuous J K
inst_8 : eqv.inverse.IsContinuous K J
φ : S ⟶ obj (eqv.functor.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (eqv.inverse.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op eqv.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := ⋯
⊢ 𝟙 R ≫ NatTrans.app (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K) R =
    ψ ≫ CategoryTheory.Functor.map (eqv.inverse.sheafPushforwardContinuous RingCat K J) φ
have h : InducedCategory.Hom.hom (𝟙 R ≫ NatTrans.app (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K) R) =
  (ψ ≫ CategoryTheory.Functor.map (eqv.inverse.sheafPushforwardContinuous RingCat K J) φ).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R_1 : Sheaf K_1 RingCat
inst_4 : F.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F.sheafPushforwardContinuous RingCat J_1 K_1) R_1
C : Type u₁
inst_5 : Category.{v₁, u₁} C
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
eqv : CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : eqv.functor.IsContinuous J K
inst_8 : eqv.inverse.IsContinuous K J
φ : S ⟶ obj (eqv.functor.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (eqv.inverse.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op eqv.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := ⋯
⊢ Eq (α := S ⟶ obj (sheafPushforwardContinuous (𝟭 C) RingCat J J) S)
    ((φ ≫ CategoryTheory.Functor.map (eqv.functor.sheafPushforwardContinuous RingCat J K) ψ) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J) S)
    (𝟙 S)
have h : InducedCategory.Hom.hom
    ((φ ≫ CategoryTheory.Functor.map (eqv.functor.sheafPushforwardContinuous RingCat J K) ψ) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J) S) =
  InducedCategory.Hom.hom (𝟙 S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X : C
⊢ Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X ∈
    (J : (a : C) → Set (Sieve a)) X
have refine : ∀ (Y : C) (hY : Y ⟶ X) (H : Sieve.arrows (Sieve.ofObjects q.X X) hY),
  Sieve.arrows
    (Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) sorry)) X)
    hY
Tactic: refine J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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
q : QuasicoherentData.{u_1, u, v₁, u₁} M
X Y : C
hY : Y ⟶ X
H : Sieve.arrows (Sieve.ofObjects q.X X) hY
⊢ Sieve.arrows
    (Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) ⋯)) X)
    hY
have obtain : ∀ (i : q.I) (hi : Y ⟶ q.X i),
  Sieve.arrows
    (Sieve.ofObjects
      (fun (i : (↑(Set.range q.X) : Type u₁)) ↦ q.X (Exists.choose (p := fun (y : q.I) ↦ q.X y = (↑i : C)) sorry)) X)
    hY
Tactic: obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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
q : QuasicoherentData.{u_1, u, v₁, u₁} M
inst_4 : q.IsFinitePresentation
⊢ ∀ (i : q.localGeneratorsData.I), (q.localGeneratorsData.generators i).IsFiniteType
have dsimp : ∀ (i : q.I), (q.presentation i).generators.IsFiniteType
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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.LocalGeneratorsData), σ.IsFiniteType
have obtain : ∀ (σ : M.QuasicoherentData), σ.IsFinitePresentation → ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType
Tactic: obtain ⟨σ, _⟩ := IsFinitePresentation.exists_quasicoherentData M
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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
⊢ Eq (α := Sieve.{v₁, u₁} x) (Sieve.ofObjects id x) ⊤
have rw : ∀ ⦃Y : C⦄ (f : Y ⟶ x), Sieve.arrows (Sieve.ofObjects id x) f ↔ Sieve.arrows ⊤ f
Tactic: rw [Sieve.ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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 (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)))
have dsimp : Presentation.IsFinite
  (Presentation.ofIsIso (Hom.over f (σ.X i)) (σ.presentation i) :
    Presentation (C := Over.{v₁, u₁} (σ.X i)) (N.over (σ.X i)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
P Q R_1 : SheafOfModules.{v, v₁, u₁, u} R
f f' : P ⟶ Q
g : Q ⟶ R_1
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
have h : ((f + f') ≫ g).val = (f ≫ g + f' ≫ g).val
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
P Q R_1 : SheafOfModules.{v, v₁, u₁, u} R
f f' : P ⟶ Q
g : Q ⟶ R_1
⊢ ((f + f') ≫ g).val = (f ≫ g + f' ≫ g).val
have h : (f.val + f'.val) ≫ g.val = f.val ≫ g.val + f'.val ≫ g.val
Tactic: dsimp