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

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (fun x1 x2 ↦ x1 ⤳ x2) y (f x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯, K := ↑(X.residueField x'),
            field := X.instFieldCarrierResidueField x', algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯,
            i₁ := X.fromSpecResidueField x', i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (fun x1 x2 ↦ x1 ⤳ x2) (l (closedPoint ↥A)) x'

Tactic:
simp_rw [← Scheme.fromSpecResidueField_apply x' (closedPoint (X.residueField x')), ← hl₁]

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (fun x1 x2 ↦ x1 ⤳ x2) y (f x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯, K := ↑(X.residueField x'),
            field := X.instFieldCarrierResidueField x', algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯,
            i₁ := X.fromSpecResidueField x', i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (fun x1 x2 ↦ x1 ⤳ x2) (l (closedPoint ↥A))
    ((Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l) (closedPoint ↑(X.residueField x')))
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 : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
⊢ awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv

Tactic:
ext z

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ (CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv))
      z
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 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
⊢ g ^ (j * d) ∈ 𝒜 (j * (d * e))

Tactic:
convert SetLike.pow_mem_graded _ hg; ring

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

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left

Tactic:
rintro ⟨T, ⟨𝒰, h, rfl⟩, hT⟩

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case h
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).arrows
    (Hom.asOver (𝒰.f i) S)

Tactic:
have p : Q (𝒰.X i ↘ S) := by
      rw [← comp_over (𝒰.f i) S]
      exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop

Goal state after:
case h
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
p : Q (𝒰.X i ↘ S)
⊢ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).arrows
    (Hom.asOver (𝒰.f i) S)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_1
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
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j : (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).I₀
⊢ Q ((Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).X j ↘ S)

Tactic:
apply MorphismProperty.Comma.prop

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 𝒜
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' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : Kmax = 0
⊢ False

Tactic:
have (i : _) : ψ i = 0 := le_zero_iff.mp (hKmax ▸ Finset.le_max' _ _ (by simp))

Goal state after:
σ : 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' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : Kmax = 0
this : ∀ (i : ι), ψ i = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Sieve.generate (Presieve.singleton (Spec.map f)) ∈ (propQCTopology P) (Spec R)

Tactic:
rw [← Hom.presieve₀_cover _ hf]

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Sieve.generate (Hom.cover (Spec.map f) hf).presieve₀ ∈ (propQCTopology P) (Spec R)
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
⊢ φ.app j ≫ colimit.ι X₂ j = φ.app j ≫ c₂.ι.app j ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom,

Goal state after:
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
⊢ φ.app j ≫ colimit.ι X₂ j = φ.app j ≫ (colimit.cocone X₂).ι.app j
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ colimit.ι S.X₂ j = S.f.app j ≫ c₂.ι.app j ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom,

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ colimit.ι S.X₂ j = S.f.app j ≫ (colimit.cocone S.X₂).ι.app j
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.g.app j ≫ colimit.ι S.X₃ j = S.g.app j ≫ c₃.ι.app j ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom,

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.g.app j ≫ colimit.ι S.X₃ j = S.g.app j ≫ (colimit.cocone S.X₃).ι.app j
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ b < ↑m → ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
intro hb

Goal state after:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Preorder α
b : α
a : Shrink.{u, u_1} α
⊢ (equivShrink α) ((equivShrink α).symm a) ≤ (equivShrink α) b ↔ (equivShrink α).symm a ≤ b

Tactic:
obtain ⟨b, rfl⟩ := (equivShrink.{u} α).symm.surjective b

Goal state after:
α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Preorder α
a b : Shrink.{u, u_1} α
⊢ (equivShrink α) ((equivShrink α).symm a) ≤ (equivShrink α) ((equivShrink α).symm b) ↔
    (equivShrink α).symm a ≤ (equivShrink α).symm b
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
h : IsMin ⊥
iter₁ iter₂ : Φ.Iteration ⊥
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ ⊥
⊢ k₂ = ⊥

Tactic:
by simpa using h₂

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
⊢ j ≤ i₂

Tactic:
by simpa using h₂

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫
      F.map (homOfLE hi) ≫ (objIso c i₂ ⋯).inv ≫ (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (objIso c i₁ ⋯).hom ≫ c.ι.app ⟨i₁, ⋯⟩ ≫ (objIsoPt c).inv =
    (objIso c i₁ ⋯).hom ≫
      F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv ≫ (objIso c i₂ hi₂₃).hom ≫ c.ι.app ⟨i₂, hi₂₃⟩ ≫ (objIsoPt c).inv

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (objIso c i₁ ⋯).hom ≫ c.ι.app ⟨i₁, ⋯⟩ ≫ (objIsoPt c).inv =
    (objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ c.ι.app ⟨i₂, hi₂₃⟩ ≫ (objIsoPt c).inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫
      F.map (homOfLE h₁₂) ≫
        (objIso F X ⟨i₂, ⋯⟩).inv ≫ (objIso F X ⟨i₂, ⋯⟩).hom ≫ F.map (homOfLE h₂₃) ≫ (objIso F X ⟨i₃, h₁⟩).inv

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ F.map (homOfLE h₂₃) ≫ (objIso F X ⟨i₃, h₁⟩).inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (ofCocone c).map (homOfLE hi) = (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv

Tactic:
by
  dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]
  rw [dif_pos hi₂]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: 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
x✝ : J
h₁ : Order.IsSuccLimit x✝
h₂ : x✝ ≤ ⊥
⊢ IsMin x✝

Tactic:
by simpa using h₂

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: 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
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) k i ⋯ hij =
    arrowι (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij) hi k hk

Tactic:
have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij

Goal state after:
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
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) k i ⋯ hij =
    arrowι (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩) =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫
      F.map (homOfLE h₁₂) ≫
        (objIso F X ⟨i₂, h₂⟩).inv ≫
          (objIso F X ⟨i₂, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩) =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫
      F.map (homOfLE h₁₂) ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
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
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f

Tactic:
have h : ⊥ < j := Ne.bot_lt' (by
      rintro rfl
      exact Order.not_isSuccLimit_bot hj)

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
h : ⊥ < j
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f