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_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:
exact R.1.map_id _

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_id
-- 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
e : SheafOfModules (C :=
    Over.{v₁, u₁}
      (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) ≌
  SheafOfModules
    (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)))) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ e.functor.obj
      (e.inverse.obj
        (over (M.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))))) ≅
    e.functor.obj
      (M.over (QuasicoherentData.X (D (i.fst (β := fun (i : I) ↦ (D i).I))) (i.snd (β := fun (i : I) ↦ (D i).I))).left)

Tactic:
exact e.counitIso.app ((M.over (X i.1)).over ((D i.1).X i.2))

Premises used: Sigma.fst, SheafOfModules.QuasicoherentData.X, SheafOfModules.over, CategoryTheory.Iso.app, Sigma.snd, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
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
inst_7 : ∀ (i : I), IsQuasicoherent (C := Over.{v₁, u₁} (X i)) (M.over (X i))
⊢ M.IsQuasicoherent

Tactic:
(QuasicoherentData.bind M X hX fun _ ↦
    IsQuasicoherent.nonempty_quasicoherentData.some).isQuasicoherent

Premises used: SheafOfModules.QuasicoherentData.isQuasicoherent, Nonempty.some, SheafOfModules.QuasicoherentData.bind, SheafOfModules.IsQuasicoherent.nonempty_quasicoherentData
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
X Y : SheafOfModules.{v, v₁, u₁, u} R
f g : X ⟶ Y
h : f.val = g.val
⊢ f = g

Tactic:
Hom.ext h

Premises used: SheafOfModules.Hom.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
X : SheafOfModules.{v, v₁, u₁, u} R
⊢ Hom.val (𝟙 X) = 𝟙 X.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
X Y Z : SheafOfModules.{v, v₁, u₁, u} R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).val = f.val ≫ g.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
⊢ (forget R).Faithful

Tactic:
(fullyFaithfulForget R).faithful

Premises used: SheafOfModules.fullyFaithfulForget, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
⊢ (forget R).Full

Tactic:
(fullyFaithfulForget R).full

Premises used: SheafOfModules.fullyFaithfulForget, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
⊢ (forget R).ReflectsIsomorphisms

Tactic:
(fullyFaithfulForget R).reflectsIsomorphisms

Premises used: SheafOfModules.fullyFaithfulForget, CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
⊢ (toSheaf R).Faithful

Tactic:
Functor.Faithful.of_comp_iso (toSheafCompSheafToPresheafIso.{v} R)

Premises used: SheafOfModules.toSheafCompSheafToPresheafIso, CategoryTheory.Functor.Faithful.of_comp_iso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
M N : SheafOfModules.{v, v₁, u₁, u} R
f g : M ⟶ N
⊢ (f + g).val = f.val + g.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
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
h : ((f + f') ≫ g).val = (f ≫ g + f' ≫ g).val
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
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
h : (f.val + f'.val) ≫ g.val = f.val ≫ g.val + f'.val ≫ g.val
⊢ ((f + f') ≫ g).val = (f ≫ g + f' ≫ g).val

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
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.val + f'.val) ≫ g.val = f.val ≫ g.val + f'.val ≫ g.val

Tactic:
simp only [Preadditive.add_comp]

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ tauto₁₁ tauto₁₂ :
  ∀ (P Q R_1 : SheafOfModules.{v, v₁, u₁, u} R) (f : P ⟶ Q) (g g' : Q ⟶ R_1), f ≫ (g + g') = f ≫ g + f ≫ g'
⊢ ∀ (P Q R_1 : SheafOfModules.{v, v₁, u₁, u} R) (f : P ⟶ Q) (g g' : Q ⟶ R_1), f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
tauto
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
M N P : SheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
g : N ⟶ P
s : M.sections
⊢ sectionsMap (f ≫ g) s = sectionsMap g (sectionsMap f s)

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMap, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
M : SheafOfModules.{v, v₁, u₁, u} R
s : M.sections
⊢ sectionsMap (𝟙 M) s = s

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMk, PresheafOfModules.sectionsMap, rfl, PresheafOfModules.sections
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  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 : SheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ Eq.{u + 1} (α :=
    (M.val.presheaf ⋙
          CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)).obj
      X)
    ((↑((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) f) :
          (j : Cᵒᵖ) → (M.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
        X :
      (M.val.presheaf ⋙
            CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).obj
        X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u))
              (RingHom.id (↑(R.obj (P := Presheaf.IsSheaf J).obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (f.val.app X) :
          (a : (↑((unit R).val.obj X) : Type u)) → (↑(M.val.obj X) : Type u))
        1 :
      (↑(M.val.obj X) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  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
f : unit R ⟶ M
p : M ⟶ N
⊢ (N.unitHomEquiv : (a : unit R ⟶ N) → N.sections) (f ≫ p) =
    sectionsMap p ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) f)

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMk, PresheafOfModules.sectionsMap, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 :
  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
s : M.sections
p : M ⟶ N
⊢ Eq (α := N.sections)
    ((N.unitHomEquiv : (a : unit R ⟶ N) → N.sections)
        ((Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) s ≫ p) :
      N.sections)
    ((N.unitHomEquiv : (a : unit R ⟶ N) → N.sections)
        ((Equiv.symm N.unitHomEquiv : (a : N.sections) → unit R ⟶ N) (sectionsMap p s)) :
      N.sections)

Tactic:
simp [unitHomEquiv_comp_apply]

Premises used: SheafOfModules.unitHomEquiv_comp_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R_1 : Sheaf J RingCat
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
N : PresheafOfModules.{v, v₁, u₁, u} R
hN : Presheaf.IsSheaf J N.presheaf
inst_1 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_2 : IsLocallySurjective J f
inst_3 : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN :
        (a : (toPresheaf R).obj M₂ ⟶ N.presheaf) → (toPresheaf R).obj M₁ ⟶ N.presheaf)
      φ =
    (toPresheaf R).map ψ
simp :
  ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            m :
          (↑(N.presheaf.obj X) : Type v))
⊢ ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
    (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
            (M₂.presheaf.obj X) (N.presheaf.obj X)
            (NatTrans.app
              (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                  (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                ((toPresheaf R).map ψ))
              X) :
          (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
        ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
                (M₂.presheaf.obj X) (N.presheaf.obj X)
                (NatTrans.app
                  (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                      (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                    ((toPresheaf R).map ψ))
                  X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            m :
          (↑(N.presheaf.obj X) : Type v))

Tactic:
simp only [← hφ, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R_1 : Sheaf J RingCat
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
N : PresheafOfModules.{v, v₁, u₁, u} R
hN : Presheaf.IsSheaf J N.presheaf
inst_1 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_2 : IsLocallySurjective J f
inst_3 : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN :
        (a : (toPresheaf R).obj M₂ ⟶ N.presheaf) → (toPresheaf R).obj M₁ ⟶ N.presheaf)
      φ =
    (toPresheaf R).map ψ
⊢ ∀ (Z : Cᵒᵖ) (x : (↑(M₁.obj Z) : Type v)),
    Eq (α := (↑(N.presheaf.obj Z) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (φ.app Z) :
            (a : (↑(((toPresheaf R).obj M₂).obj Z) : Type v)) → (↑(N.presheaf.obj Z) : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (f.app Z) :
                (a : (↑(M₁.obj Z) : Type v)) → (↑(M₂.obj Z) : Type v))
              x :
            (↑(M₂.obj Z) : Type v)) :
        (↑(N.presheaf.obj Z) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (ψ.app Z) :
            (a : (↑(M₁.obj Z) : Type v)) → (↑(N.obj Z) : Type v))
          x :
        (↑(N.obj Z) : Type v))

Tactic:
replace hφ : ∀ (Z : Cᵒᵖ) (x : M₁.obj Z), φ.app Z (f.app Z x) = ψ.app Z x :=
          fun Z x ↦ CategoryTheory.congr_fun (congr_app hφ Z) x
-- Module: Mathlib.Algebra.Category.ModuleCat.Simple
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : IsSimpleOrder (Subobject (C := ModuleCat.{u_2, u_1} R) (of R M)) ↔ IsSimpleModule R M
rw₁ : IsSimpleOrder.{u_2} (Submodule R (↑(of R M) : Type u_2)) ↔ IsSimpleModule R M
rw₂ rw₃ : IsSimpleOrder.{u_2} (Submodule R (↑(of R M) : Type u_2)) ↔ IsSimpleOrder.{u_2} (Submodule R M)
⊢ Simple (C := ModuleCat.{u_2, u_1} R) (of R M) ↔ IsSimpleModule R M

Tactic:
rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff,
    isSimpleModule_iff]

Premises used: CategoryTheory.simple_iff_subobject_isSimpleOrder, ModuleCat.of, isSimpleModule_iff, ModuleCat.subobjectModule, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.Simple
Goal:
R : Type u_1
inst : Ring R
M : ModuleCat.{u_3, u_1} R
⊢ Simple M ↔ IsSimpleModule.{u_1, u_3} R (↑M : Type u_3)

Tactic:
simple_iff_isSimpleModule

Premises used: simple_iff_isSimpleModule
-- Module: Mathlib.Algebra.Category.ModuleCat.Simple
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
⊢ Simple (C := ModuleCat.{u_2, u_1} R) (of R M)

Tactic:
simple_iff_isSimpleModule.mpr ‹_›

Premises used: Iff.mpr, simple_iff_isSimpleModule
-- Module: Mathlib.Algebra.Category.ModuleCat.Simple
Goal:
R : Type u_1
M_1 : Type u_2
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M : ModuleCat.{u_3, u_1} R
inst_3 : Simple M
⊢ IsSimpleModule.{u_1, u_3} R (↑M : Type u_3)

Tactic:
simple_iff_isSimpleModule.mp ‹_›

Premises used: simple_iff_isSimpleModule, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.Simple
Goal:
R : Type u_1
inst : Ring R
k : Type u_3
inst_1 : Field k
inst_2 : Algebra k R
V : ModuleCat.{u_4, u_1} R
h : finrank.{u_3, u_4} k (↑V : Type u_4) = 1
⊢ Simple V

Tactic:
(simple_iff_isSimpleModule' V).mpr <| (isSimpleModule_iff ..).mpr <|
    is_simple_module_of_finrank_eq_one h

Premises used: Iff.mpr, isSimpleModule_iff, is_simple_module_of_finrank_eq_one, simple_iff_isSimpleModule'
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : (↑X : Type u)
i : (OpenNhds x)ᵒᵖ
dsimp :
  Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
⊢ Module (↑(((OpenNhds.inclusion x).op ⋙ R).obj i) : Type u)
    (↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) : Type u)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : (↑X : Type u)
i : (OpenNhds x)ᵒᵖ
⊢ Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : (↑X : Type u)
U : Opens (↑X : Type u)
hx : x ∈ U
r : (↑(R.obj (op U)) : Type u)
m : (↑(M.obj (op U)) : Type u)
i : (OpenNhds x)ᵒᵖ
dsimp :
  Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
⊢ Module (↑(((OpenNhds.inclusion x).op ⋙ R).obj i) : Type u)
    (↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) : Type u)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : (↑X : Type u)
U : Opens (↑X : Type u)
hx : x ∈ U
r : (↑(R.obj (op U)) : Type u)
m : (↑(M.obj (op U)) : Type u)
i : (OpenNhds x)ᵒᵖ
⊢ Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)

Tactic:
infer_instance