awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
⊢ Eq (α := I → N.sections)
    ((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
        ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) s ≫ p : free I ⟶ N) :
      I → N.sections)
    ((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
        ((Equiv.symm N.freeHomEquiv : (a : I → N.sections) → free I ⟶ N) fun (i : I) ↦ sectionsMap p (s i)) :
      I → N.sections)
have h : ∀ (x : I) (X : Cᵒᵖ),
  Eq.{u + 1} (α :=
    (N.val.presheaf ⋙
          CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)).obj
      X)
    ((↑((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
            ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) s ≫ p : free I ⟶ N) x) :
        (j : Cᵒᵖ) → (N.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
      X)
    ((↑((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
            ((Equiv.symm N.freeHomEquiv : (a : I → N.sections) → free I ⟶ N) fun (i : I) ↦ sectionsMap p (s i)) x) :
        (j : Cᵒᵖ) → (N.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
      X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I J : Type u
f : I → J
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free J))
    ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J)
        ((freeHomEquiv (free J) : (a : free I ⟶ free J) → I → (free J).sections) (freeMap f)) :
      Quiver.Hom (V := SheafOfModules R) (free I) (free J))
    ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J) (freeSection ∘ f) :
      Quiver.Hom (V := SheafOfModules R) (free I) (free J))
have simp : Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free J)) (freeMap f)
  ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J) (freeSection ∘ f))
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I : Type u
M : SheafOfModules R
f : I → M.sections
i : I
⊢ sectionsMap (M := free I) ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) f) (freeSection i) = f i
have obtain : ∀ (f : free I ⟶ M),
  Eq (α := M.sections)
    (sectionsMap (M := free I)
      ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M)
        ((M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f))
      (freeSection i))
    ((M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f i)
Tactic: obtain ⟨f, rfl⟩ := (freeHomEquiv M).surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I J : Type u
f : I → J
i : I
⊢ Eq (α := unit R ⟶ free J) (ιFree i ≫ freeMap f) (ιFree (f i))
have rw : Eq (α := unit R ⟶ free J)
  ((Equiv.symm (unitHomEquiv (free J)) : (a : (free J).sections) → unit R ⟶ free J) ((freeSection ∘ f) i) :
    unit R ⟶ free J)
  (ιFree (f i) : unit R ⟶ free J)
Tactic: rw [← unitHomEquiv_symm_freeHomEquiv_apply, freeHomEquiv_freeMap]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I J : Type u
f : I → J
i : I
⊢ Eq (α := unit R ⟶ free J)
    ((Equiv.symm (unitHomEquiv (free J)) : (a : (free J).sections) → unit R ⟶ free J)
        ((freeHomEquiv (free J) : (a : free J ⟶ free J) → J → (free J).sections) (𝟙 (free J)) (f i)) :
      unit R ⟶ free J)
    (ιFree (f i) : unit R ⟶ free J)
have rw : Eq (α := unit R ⟶ free J) (ιFree (f i) ≫ 𝟙 (free J)) (ιFree (f i))
Tactic: rw [unitHomEquiv_symm_freeHomEquiv_apply, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I J : Type u
f : I → J
i : I
rw : Eq (α := unit R ⟶ free J) (ιFree (f i) ≫ 𝟙 (free J)) (ιFree (f i))
⊢ Eq (α := unit R ⟶ free J)
    ((Equiv.symm (unitHomEquiv (free J)) : (a : (free J).sections) → unit R ⟶ free J)
        ((freeHomEquiv (free J) : (a : free J ⟶ free J) → J → (free J).sections) (𝟙 (free J)) (f i)) :
      unit R ⟶ free J)
    (ιFree (f i) : unit R ⟶ free J)
have rw₁ : Eq (α := unit R ⟶ free J) (ιFree (f i)) (ιFree (f i))
Tactic: rw [unitHomEquiv_symm_freeHomEquiv_apply, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I J : Type u
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free (I ⊕ J))) (coprod.inl ≫ Iso.hom (freeSumIso I J))
    (freeMap Sum.inl)
have rw : Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free (I ⊕ J))) (coprod.inl ≫ Iso.hom (freeSumIso I J))
  (CategoryTheory.Functor.map freeFunctor (↾Sum.inl))
Tactic: rw [← dsimp% freeFunctor_map (↾(Sum.inl : I → I ⊕ J))]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
I J : Type u
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free J) (free (I ⊕ J))) (coprod.inr ≫ Iso.hom (freeSumIso I J))
    (freeMap Sum.inr)
have rw : Eq (α := Quiver.Hom (V := SheafOfModules R) (free J) (free (I ⊕ J))) (coprod.inr ≫ Iso.hom (freeSumIso I J))
  (CategoryTheory.Functor.map freeFunctor (↾Sum.inr))
Tactic: rw [← dsimp% freeFunctor_map (↾(Sum.inr : J → I ⊕ J))]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators (goal)
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst_4 : Epi p
⊢ Epi (C := SheafOfModules R) (X := free σ.I) (Y := N)
    ((Equiv.symm N.freeHomEquiv : (a : σ.I → N.sections) → free σ.I ⟶ N) fun (i : σ.I) ↦ sectionsMap p (σ.s i))
have rw : Epi (X := free σ.I) (Y := N)
  ((Equiv.symm M.freeHomEquiv : (a : σ.I → M.sections) → free σ.I ⟶ M) σ.s ≫ p : free σ.I ⟶ N)
Tactic: rw [← freeHomEquiv_symm_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators (goal)
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := 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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.Generators (goal)
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
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))
M_1 N P : SheafOfModules R
inst_4 : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst_5 :
  ∀ (X : C),
    (J.over X).WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦
      (↑x1 : Type u) →+ (↑x2 : Type u)) (CA := 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))
M : SheafOfModules R
q : LocalGeneratorsData.{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.Localization (goal)
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
⊢ inverseImage J.W (toPresheaf R₀) = inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α)
have rw : inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) =
  inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α)
Tactic: rw [J.W_eq_inverseImage_isomorphisms]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization (goal)
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
⊢ inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) =
    inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α)
have h : ∀ ⦃P Q : PresheafOfModules.{v, v', u', u} R₀⦄ (f : P ⟶ Q),
  inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) f ↔
    inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α) f
Tactic: ext P Q f
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization (goal)
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
P Q : PresheafOfModules.{v, v', u', u} R₀
f : P ⟶ Q
⊢ inverseImage (inverseImage (isomorphisms (Sheaf J Ab)) (presheafToSheaf J Ab)) (toPresheaf R₀) f ↔
    inverseImage (isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α) f
have h : IsIso (X := Functor.obj (presheafToSheaf J Ab) ((toPresheaf R₀).obj P))
    (CategoryTheory.Functor.map (presheafToSheaf J Ab) ((toPresheaf R₀).map f)) ↔
  IsIso ((SheafOfModules.toSheaf R).map ((sheafification α).map f))
Tactic: simp only [inverseImage_iff, isomorphisms.iff,
    ← isIso_iff_of_reflects_iso _ (SheafOfModules.toSheaf.{v} R)]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization (goal)
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 J.W (toPresheaf R₀))
have rw : (sheafification α).IsLocalization
  (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (SheafOfModules.{v, v', u', u} R)) (sheafification α))
Tactic: rw [inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms α]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree (goal)
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
⊢ 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))
have 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)
Tactic: ext X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree (goal)
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
⊢ IsIso (X := (pullback φ).obj (unit S)) (Y := unit R) (pullbackObjUnitToUnit φ)
have rw : ∀ (T : SheafOfModules R),
  Function.Bijective (β := (pullback φ).obj (unit S) ⟶ T) fun (x : unit R ⟶ T) ↦ pullbackObjUnitToUnit φ ≫ x
Tactic: rw [isIso_iff_coyoneda_map_bijective]