mathlib-initiative/mathlib-tactics huggingface dataset:
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
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩),
    ((presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫
          G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫
        G₀.obj.map I.f.op =
      ((presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫
          G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫
        G₀.obj.map I.f.op

Tactic:
intro ⟨U₀, c, ⟨j, t, fac₁, fac₂⟩⟩

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₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
U₀ : C₀
c : U₀ ⟶ W₀
j : (data X).I₁ i₁ i₂
t : U₀ ⟶ (data X).Y j
fac₁ : c ≫ b₁ = t ≫ (data X).p₁ j
fac₂ : c ≫ b₂ = t ≫ (data X).p₂ j
⊢ ((presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫
      G₀.obj.map { Y := U₀, f := c, hf := ⋯ }.f.op =
    ((presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫
        G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫
      G₀.obj.map { Y := U₀, f := c, hf := ⋯ }.f.op
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₂
⊢ ⋯.HasLift

Tactic:
obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜

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 = ⊤
hx' : ∀ i ∈ x, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
⊢ ⋯.HasLift
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
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Surjective ((∐ 𝒰.X).isoSpec.inv ≫ Sigma.desc 𝒰.f)

Tactic:
have : Surjective (Sigma.desc 𝒰.f) := inferInstanceAs <| Surjective (Sigma.desc 𝒰.forgetQc.f)

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this✝ : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
this : Surjective (Sigma.desc 𝒰.f)
⊢ Surjective ((∐ 𝒰.X).isoSpec.inv ≫ Sigma.desc 𝒰.f)
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
t : F.obj.obj X
⊢ J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) t) =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := J.uliftYonedaEquiv.surjective t
  rw [uliftYonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Goal state after:
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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst✝ : IsFiltered J
j : Under j₀
⊢ (colimit.cocone
              { X₁ := kernel (g y), X₂ := (Functor.const (Under j₀)).obj X, X₃ := Under.forget j₀ ⋙ Y,
                  f := kernel.ι (g y), g := g y, zero := ⋯ }.X₁).ι.app
        j ≫
      f y =
    { X₁ := kernel (g y), X₂ := (Functor.const (Under j₀)).obj X, X₃ := Under.forget j₀ ⋙ Y, f := kernel.ι (g y),
              g := g y, zero := ⋯ }.f.app
        j ≫
      (constCocone (Under j₀) X).ι.app j

Tactic:
by simpa using! hf y j

Goal state after:
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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst✝ : IsFiltered J
x✝ : Under j₀
⊢ (constCocone (Under j₀) X).ι.app x✝ ≫ 0 =
    { X₁ := kernel (g y), X₂ := (Functor.const (Under j₀)).obj X, X₃ := Under.forget j₀ ⋙ Y, f := kernel.ι (g y),
              g := g y, zero := ⋯ }.g.app
        x✝ ≫
      (Cocone.whisker (Under.forget j₀) c).ι.app x✝

Tactic:
simpa using! hy.symm

Goal state after:
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 : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
⊢ (colimit.cocone (kernel (g y))).ι.app j ≫ f y = ((F y).obj j).obj.hom

Tactic:
by simpa using! hf y j

Goal state after:
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) ?_)

Goal state after:
case refine_1
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
⊢ Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z))) ≅ Arrow.mk (f z)

case refine_2
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
⊢ MorphismProperty.isomorphisms C (colim.map c.ι)
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯))

Tactic:
← homOfLE_comp bot_le (Order.le_succ j),

Goal state after:
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯ ≫ homOfLE ⋯))
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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
⊢ IsColimit (coconeOfLE iter.F hij)

Tactic:
letI := hasColimitsOfShape_of_isSuccLimit C i hi
  refine IsColimit.ofIsoColimit (colimit.isColimit (restrictionLT iter.F hij))
    (Cocone.ext (eqToIso (iter.obj_limit i hi hij).symm) ?_)
  rintro ⟨k, hk⟩
  apply Arrow.mk_injective
  dsimp
  rw [← arrowMap]
  simp [iter.arrowMap_limit i hi hij k hk, arrowι_def]

Goal state after:
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
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj ⟨k₂, h₂⟩ = F.obj ⟨k₂, h₂⟩

Tactic:
h.tgt

Goal state after:
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
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj ⟨k₂, h₂⟩ = G.obj ⟨k₂, h₂⟩
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
⊢ F = G

Tactic:
apply Arrow.functor_ext
  rintro ⟨k₁, _⟩ ⟨k₂, h₂⟩ f
  apply h

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

Goal state before:
pp: case neg
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
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ (if h₁ : Order.succ j ≤ j then
      (objIso F X ⟨Order.succ j, ⋯⟩).hom ≫ F.map (𝟙 ⟨Order.succ j, ⋯⟩) ≫ (objIso F X ⟨Order.succ j, h₁⟩).inv
    else
      if h₂ : Order.succ j ≤ j then
        (objIso F X ⟨Order.succ j, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)) =
    𝟙 (obj F X ⟨Order.succ j, ⋯⟩)

Tactic:
rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
      dif_neg h₁]

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

Goal state before:
pp: case inl.inr
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₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃

Tactic:
map_id,

Goal state after:
case inl.inr
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₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ 𝟙 (obj c i₂)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inr
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₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃

Tactic:
map_id,

Goal state after:
case inr
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₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = 𝟙 (obj c i₁) ≫ map c i₁ i₃ hi' hi₃
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
⊢ (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi)

Tactic:
Iso.inv_hom_id,

Goal state after:
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
⊢ (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ 𝟙 (F.obj ⟨i₂, hi₂⟩) =
    (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg.inr
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₁ : J
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h

Tactic:
map_id,

Goal state after:
case neg.inr
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₁ : J
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: 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
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫
      F.map (homOfLE ⋯) ≫ (extendToSucc.objIso F X ⟨i₂, hi₂⟩).inv ≫ (extendToSucc.objIso F X ⟨i₂, hi₂⟩).hom =
    (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE hi)

Tactic:
Iso.inv_hom_id,

Goal state after:
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
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ 𝟙 (F.obj ⟨i₂, hi₂⟩) =
    (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE hi)
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
f : Arrow C
hf✝ : f ∈ ⋃ i, (W i).toSet
hf : ∃ i, f ∈ (W i).toSet
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, f⟩ => ⟨↑f, ⋯⟩)
        a =
      ⟨f, hf✝⟩

Tactic:
obtain ⟨i, hf⟩ := hf

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
f : Arrow C
hf✝ : f ∈ ⋃ i, (W i).toSet
i : α
hf : f ∈ (W i).toSet
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, f⟩ => ⟨↑f, ⋯⟩)
        a =
      ⟨f, hf✝⟩
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
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
f✝ : F.obj ⊥ ⟶ X
g✝ : ((Functor.const J).obj c.pt).obj ⊥ ⟶ Y
sq : CommSq f✝ (c.ι.app ⊥) p g✝
j : J
hj : ¬IsMax j
x✝¹ : F.obj j ⟶ X
x✝ : CommSq x✝¹ (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
⊢ x✝.HasLift

Tactic:
have := hF j 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
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
f✝ : F.obj ⊥ ⟶ X
g✝ : ((Functor.const J).obj c.pt).obj ⊥ ⟶ Y
sq : CommSq f✝ (c.ι.app ⊥) p g✝
j : J
hj : ¬IsMax j
x✝¹ : F.obj j ⟶ X
x✝ : CommSq x✝¹ (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
this : HasLiftingProperty (F.map (homOfLE ⋯)) p
⊢ x✝.HasLift
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e'_2
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    (ConcreteCategory.hom (F.map (𝟙 (op (Order.succ i))))) (e (Order.succ i) ⋯).val

Tactic:
map_id,

Goal state after:
case e'_2
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    (ConcreteCategory.hom (𝟙 (F.obj (op (Order.succ i))))) (e (Order.succ i) ⋯).val
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this : LocallySmall.{w, v, u} C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
have := isSmall I κ

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this✝ : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this : LocallySmall.{w, v, u} C
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)

Tactic:
have := isSmall I κ

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝ : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this :
  (ConcreteCategory.hom (F.map (𝟙 (op i)))) (e i hij').val =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩

Tactic:
map_id,

Goal state after:
case inl
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this :
  (ConcreteCategory.hom (𝟙 (F.obj (op i)))) (e i hij').val =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inr
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ (ConcreteCategory.hom (F.map (𝟙 (op i)))) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩

Tactic:
map_id,

Goal state after:
case inr
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ (ConcreteCategory.hom (𝟙 (F.obj (op i)))) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩