mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
x✝ : ↥(Opposite.unop (Opposite.op V))
⊢ val (↑⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑0, ⋯⟩ x✝) = val (↑0 x✝)

Tactic:
simp [comapStructureSheafFun]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
x y : ↑((structureSheaf 𝒜).obj.obj (Opposite.op U))
x✝ : ↥(Opposite.unop (Opposite.op V))
⊢ val (↑⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑(x + y), ⋯⟩ x✝) =
    val
      (↑(⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑x, ⋯⟩ +
            ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑y, ⋯⟩)
        x✝)

Tactic:
simp [comapStructureSheafFun]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case hy.refine_3
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ val (Away.mk 𝒜 hf (dv j) (∏ i, v i ^ Pi.single j d i) ⋯) = val (isLocalizationElem hf ⋯)

Tactic:
simp [Pi.single_apply]

Goal state after:
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk (a ^ m * ↑(((decompose 𝒜) x) (i - n)) ^ m) ⟨f ^ i, ⋯⟩ =
    Localization.mk (a ^ m * ↑(((decompose 𝒜) x) (i - n)) ^ m) (⟨f ^ n, ⋯⟩ * ⟨f ^ (i - n), ⋯⟩)

Tactic:
· congr; rw [← pow_add, Nat.add_sub_of_le h]

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Function.Injective (Subtype.val ∘ ⇑(g.rangeRestrict.comp f))

Tactic:
convert! (IsFractionRing.injective R K); rw [← h]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ ?mp.a✝ ≤ topologically @SpecializingMap

Tactic:
apply specializingMap

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 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ IsClosedImmersion
    (Cover.pullbackHom
      (Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
        (toSpecZero 𝒜))
      (diagonal (toSpecZero 𝒜)) (i, j))

Tactic:
dsimp [Scheme, Cover.pullbackHom]

Goal state after:
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ IsClosedImmersion
    (snd (diagonal (toSpecZero 𝒜))
      ((Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover (toSpecZero 𝒜)
            (toSpecZero 𝒜)).f
        (i, j)))
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
⊢ ⋯.HasLift

Tactic:
let S'l₂ : S'.commSq.LiftStruct := ⟨S.i₂ ≫ pullback.snd f f,
      by simp [S', ← S.commSq.w_assoc], by simp [S', pullback.condition]⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this : Nonempty ι
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
let Kmax := (Finset.univ.image ψ).max' (by simp)

Goal state after:
case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀ (G_1 : Cᵒᵖ ⥤ A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g

Tactic:
ext ⟨X⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀ (G_1 : Cᵒᵖ ⥤ A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
⊢ f.app (op X) = g.app (op X)
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
⊢ presheafMap data G₀ (𝟙 X) = 𝟙 (presheafObj data G₀ X)

Tactic:
ext i
  rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (generate (Presieve.ofArrows X π)).arrows.cocone)
⊢ EffectiveEpiFamily X π

Tactic:
Sieve.generateFamily_eq

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (generateFamily X π).arrows.cocone)
⊢ EffectiveEpiFamily X π
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
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (generate (Presieve.ofArrows X π)).arrows.cocone)

Tactic:
Sieve.generateFamily_eq

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (generateFamily X π).arrows.cocone)
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
hR : R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = R

Tactic:
by
  rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
  obtain ⟨𝒰, rfl⟩ := hR
  let 𝒱 : PreZeroHypercover X :=
    ⟨𝒰.I₀, fun i ↦ Over.mk _ (𝒰.X i).hom ?_, fun i ↦ Over.homMk (𝒰.f i).left (by simp) trivial⟩
  · use 𝒱.presieve₀
    rw [Presieve.map_ofArrows]
    rfl
  · rw [← CategoryTheory.Over.w (𝒰.f i)]
    exact P.comp_mem _ _ (H _ 𝒰.mem₀ ⟨⟨i⟩⟩) X.prop

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₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i : (data (F.obj X₀)).I₀
d : F.obj T₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac₂ : d ≫ (data (F.obj X₀)).f i = F.map (c ≫ b)
⊢ d ≫ (data (F.obj X₀)).f i = F.map (c ≫ a) ≫ f

Tactic:
rw [fac₂, map_comp, map_comp_assoc, fac₁]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
⊢ (Sieve.ofArrows X c.inj).functor ⟶ s.pt.obj

Tactic:
refine ⟨fun Y ↦ ↾fun g ↦ ((s.inj (Sieve.ofArrows.i g.2)).hom.app Y)
      (Sieve.ofArrows.h g.2), ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
⊢ ∀ ⦃X_1 Y : Cᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Sieve.ofArrows X c.inj).functor.map f ≫
        ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯)) =
      (↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app X_1)) (Sieve.ofArrows.h ⋯)) ≫ s.pt.obj.map f
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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ y₁ ≫ c.ι.app j₀ - y₂ ≫ c.ι.app j₀ = 0

Tactic:
sub_eq_zero,

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
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case pos
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : Function.Surjective ⇑f
⊢ HasColimitsOfShape α C

pp: case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
⊢ HasColimitsOfShape α C

Tactic:
· exact hasColimitsOfShape_of_equivalence
      (OrderIso.ofRelIsoLT (RelIso.ofSurjective f.toRelEmbedding hf)).equivalence.symm

Goal state after:
case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
⊢ HasColimitsOfShape α C
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg.isMin
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
hi : IsMin s.top
⊢ HasColimitsOfShape α C

Tactic:
exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) = ↑⟨Order.pred ↑i, ⋯⟩

Tactic:
simp only [coe_pred_of_not_isMin hi]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ Monotone fun W ↦ W.transfiniteCompositionsOfShape J

Tactic:
rintro _ _ h _ _ _ ⟨t⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
t : a✝.TransfiniteCompositionOfShape J f✝
⊢ b✝.transfiniteCompositionsOfShape J f✝
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map (⋯.functor.map f.unop).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val

Tactic:
← comp_apply,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (⋯.functor.map f.unop).op)) val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) = val₀

Tactic:
← comp_apply,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op)) e.val = val₀
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val))

Tactic:
← comp_apply,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op)) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val))
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val))

Tactic:
← comp_apply,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op)) e.val)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hki).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩

Tactic:
← comp_apply,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE hki).op)) e.val =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val)

Tactic:
← comp_apply,

Goal state after:
case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val =
    (ConcreteCategory.hom (F.map (homOfLE hij).op ≫ F.map (homOfLE ⋯).op)) e.val