mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ Submonoid.powers (unop r) ≤
    Submonoid.comap
      (algebraMap (↑R)
        (Module.End ↑R
          ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                  (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
              r)))
      (IsUnit.submonoid
        (Module.End ↑R
          ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                  (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
              r)))

Tactic:
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ IsUnit
    ((algebraMap (↑R)
        (Module.End ↑R
          ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                  (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
              r)))
      (unop r))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ Submonoid.powers (unop r) ≤
    Submonoid.comap
      (algebraMap (↑R)
        (Module.End ↑R
          ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
      (IsUnit.submonoid
        (Module.End ↑R
          ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))

Tactic:
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]

Goal state after:
case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ IsUnit
    ((algebraMap (↑R)
        (Module.End ↑R
          ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
      (unop r))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x✝² x✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HomogeneousLocalization.val (↑⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) (x✝² * x✝¹), ⋯⟩ x✝) =
    HomogeneousLocalization.val
      (↑(⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝², ⋯⟩ * ⟨fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) x✝¹, ⋯⟩)
        x✝)

Tactic:
simp only [map_mul, HomogeneousLocalization.val_mul, Proj.mul_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_2.refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
Y : ↥X.left → Q.Over ⊤ S
f : (x : ↥X.left) → Y x ⟶ X
y : (x : ↥X.left) → ↥(Y x).left
hf : ∀ (x : ↥X.left), R.arrows (f x)
hP : ∀ (x : ↥X.left), P (f x).left
hy : ∀ (x : ↥X.left), (f x).left (y x) = x
𝒰 : Cover (precoverage P) X.left := { I₀ := ↥X.left, X := fun i ↦ (Y i).left, f := fun i ↦ (f i).left, mem₀ := ⋯ }
this : Cover.Over S 𝒰 := { over := fun i ↦ inferInstance, isOver_map := ⋯ }
⊢ 𝒰.toPresieveOverProp ⋯ ≤ R.arrows

Tactic:
· rintro - - ⟨i⟩
      exact hf i

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
B : Type u''
inst✝⁴ : Category.{v'', u''} B
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasColimitsOfSize.{w, w, v'', u''} B
F : A ⥤ B
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F
X : C
x : Φ.fiber.obj X
P : Cᵒᵖ ⥤ A
this : PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ F
⊢ Φ.toPresheafFiber X x (P ⋙ F) ≫ (Φ.presheafFiberCompIso F).hom.app P = F.map (Φ.toPresheafFiber X x P)

Tactic:
simp only [presheafFiberCompIso]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
B : Type u''
inst✝⁴ : Category.{v'', u''} B
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasColimitsOfSize.{w, w, v'', u''} B
F : A ⥤ B
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F
X : C
x : Φ.fiber.obj X
P : Cᵒᵖ ⥤ A
this : PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ F
⊢ Φ.toPresheafFiber X x (P ⋙ F) ≫
      (((Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A).obj (CategoryOfElements.π Φ.fiber).op).isoWhiskerLeft
              (preservesColimitNatIso F).symm).hom.app
        P =
    F.map (Φ.toPresheafFiber X x P)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ IsLocalizing (modulesSpecToSheaf.obj M)

Tactic:
isLocalizing_iff_aux

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ Aux M ⊤
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres✝ : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
i : Sigma κ
t : ↑(PrimeSpectrum.basicOpen (a i.fst i.snd)) ⟶ ↑(U ↑i.fst) := (Spec R).homOfLE ⋯
iso : restrictFunctor (U ↑i.fst).ι ⋙ restrictFunctor ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) ≅
  restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd))))) :=
  (restrictFunctorComp ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (U ↑i.fst).ι).symm ≪≫ restrictFunctorCongr ⋯
pres : SheafOfModules.Presentation
  ((restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))).obj M) :=
  SheafOfModules.Presentation.ofIsIso (iso.app M).hom
    (presentationRestrict ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (pres✝ ↑i.fst))
this :
  IsLocalizing
    (modulesSpecToSheaf.obj
      (M.restrict (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))))
⊢ Aux M (PrimeSpectrum.basicOpen (a i.fst i.snd))

Tactic:
isLocalizing_iff_aux

Goal state after:
case refine_2
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres✝ : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
i : Sigma κ
t : ↑(PrimeSpectrum.basicOpen (a i.fst i.snd)) ⟶ ↑(U ↑i.fst) := (Spec R).homOfLE ⋯
iso : restrictFunctor (U ↑i.fst).ι ⋙ restrictFunctor ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) ≅
  restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd))))) :=
  (restrictFunctorComp ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (U ↑i.fst).ι).symm ≪≫ restrictFunctorCongr ⋯
pres : SheafOfModules.Presentation
  ((restrictFunctor (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))).obj M) :=
  SheafOfModules.Presentation.ofIsIso (iso.app M).hom
    (presentationRestrict ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) (pres✝ ↑i.fst))
this : Aux (M.restrict (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd)))))) ⊤
⊢ Aux M (PrimeSpectrum.basicOpen (a i.fst i.snd))
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g

Tactic:
rintro ⟨a, g, rfl⟩
    exact ⟨_, g, π a, ⟨a⟩, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
⊢ ⋯.HasLift

Tactic:
have H : Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
      CommRingCat.ofHom (fromZeroRingHom 𝒜 _) ≫ Spec.preimage φ := by
    apply Spec.map_injective
    simp only [Spec.map_comp, Spec.map_preimage, ← w.w]
    rw [← Proj.awayι_toSpecZero _ _ (hxd i i.2), IsOpenImmersion.lift_fac_assoc]
    exact Nat.zero_lt_of_ne_zero (hd i i.2)

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_2
X : Scheme
⊢ ∀ {R S : CommRingCat} (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
intro R

Goal state after:
case refine_2
X : Scheme
R : CommRingCat
⊢ ∀ {S : CommRingCat} (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf TopCat.grothendieckTopology (yoneda.obj (TopCat.of (ULift.{u_1, v} T)))

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf TopCat.grothendieckTopology (yoneda.obj (TopCat.of (ULift.{u_1, v} T)))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_1
T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
← isSheaf_iff_isSheaf_of_type

Goal state after:
case refine_1
T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_1
T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]
    exact isSheaf_zariskiTopology_continuousMapPresheaf _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
⊢ presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀ = 𝟙 (G₀.obj.obj (op X₀))

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, cover_lift F J₀ _ (data (F.obj X₀)).mem₀⟩ _ _ ?_

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀, ⋯⟩),
    (presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀) ≫ G₀.obj.map I.f.op =
      𝟙 (G₀.obj.obj (op X₀)) ≫ G₀.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
⊢ Presheaf.IsSheaf J (presheaf data G₀)

Tactic:
isSheaf_iff data

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
⊢ Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀) ∧
    ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ x₄ = 0

Tactic:
have fac₃ : (-x₂) ≫ r' = x₃ ≫ b' := by
      rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ c₁.ι.app j ≫ (hc₁.coconePointUniqueUpToIso (colimit.isColimit X₁)).hom ≫ (Arrow.mk (colim.map φ)).hom =
    c₁.ι.app j ≫ (Arrow.mk f).hom ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom

Tactic:
dsimp
      rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
h : Epi f
this✝ : IsFiltered J
this : Mono f
⊢ ∃ j, IsIso (F.obj j).obj.hom

Tactic:
Subobject.epi_iff_mk_eq_top f,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : Subobject.mk f = ⊤
⊢ ∃ j, IsIso (F.obj j).obj.hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ IsIso (f z)

Tactic:
refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
    (MorphismProperty.of_isPullback
      ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)
  · refine Arrow.isoMk (Iso.refl _)
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isColimitConstCocone J X)) ?_
    dsimp
    ext j
    rw [Category.id_comp, ι_colimMap_assoc, colimit.comp_coconePointUniqueUpToIso_hom,
      constCocone_ι, NatTrans.id_app, Category.comp_id]
    apply hf
  · refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).2
      ((inferInstance : IsIso (𝟙 c.pt)))
    exact Arrow.isoMk (IsColimit.coconePointUniqueUpToIso (colimit.isColimit Y) hc)
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
        (isColimitConstCocone J c.pt))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presheaf.IsSheaf K (CategoryTheory.uliftYoneda.{v, v', u_1}.obj (F.obj Y))

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presieve.IsSheaf K (CategoryTheory.uliftYoneda.{v, v', u_1}.obj (F.obj Y))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f → Arrow.mk f = Φ.toSuccArrow X

Tactic:
rintro ⟨_⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X✝ X Y : C
⊢ Arrow.mk (Φ.toSucc X✝) = Φ.toSuccArrow X✝
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter l₂ pf✝⁷).F l₁ l₂ pf✝⁵ pf✝³ = arrowMap (functor hj iter) (↑⟨l₁, pf✝²⟩) (↑⟨l₂, pf✝¹⟩) pf✝ pf✝¹

Tactic:
arrowMap_functor _ _ _ _ _ hl₂,

Goal state after:
case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter l₂ pf✝⁷).F l₁ l₂ pf✝⁵ pf✝³ = Arrow.mk ((iter ↑⟨l₁, pf✝²⟩ ⋯).mapObj (iter l₂ hl₂) pf✝ ⋯ ⋯ pf✝)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case isMin
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
hi : IsMin ⊥
⊢ Nonempty (Φ.Iteration ⊥)

Tactic:
exact ⟨mkOfBot Φ J⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
ι : Type t
inst✝ : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : ι → ↑(ofHoms f).toSet := fun i ↦ ⟨Arrow.mk (f i), ⋯⟩
⊢ IsSmall.{w, v, u} (ofHoms f)

Tactic:
have hφ : Function.Surjective φ := by
    rintro ⟨⟨_, _, f⟩, ⟨i⟩⟩
    exact ⟨i, rfl⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
ι : Type t
inst✝ : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : ι → ↑(ofHoms f).toSet := fun i ↦ ⟨Arrow.mk (f i), ⋯⟩
hφ : Function.Surjective φ
⊢ IsSmall.{w, v, u} (ofHoms f)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g✝ : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g✝).sections
i i' : ↑(Set.Iio j)
g : i ⟶ i'
this :
  ((ConcreteCategory.hom ((⋯.functor.op ⋙ sqFunctor c p f g✝).map g.op)) (↑s (Opposite.op i'))).f' =
    (↑s (Opposite.op i)).f'
⊢ (⋯.functor ⋙ F).map g ≫ (↑s (Opposite.op i')).f' =
    (↑s (Opposite.op i)).f' ≫ ((Functor.const ↑(Set.Iio j)).obj X).map g

Tactic:
dsimp at this ⊢

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g✝ : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g✝).sections
i i' : ↑(Set.Iio j)
g : i ⟶ i'
this : F.map (⋯.functor.map g) ≫ (↑s (Opposite.op i')).f' = (↑s (Opposite.op i)).f'
⊢ F.map (⋯.functor.map g) ≫ (↑s (Opposite.op i')).f' = (↑s (Opposite.op i)).f' ≫ 𝟙 X