mathlib-initiative/mathlib-tactics huggingface dataset:
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]

Goal state after:
case refine_1
T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T)
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
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
i : 𝒰.I₀
⊢ Over.Hom.left (𝒰.f i) ≫ X.hom = (Over.mk ⊤ (𝒰.X i).hom ⋯).hom

Tactic:
simp

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

Goal state before:
pp: S : Scheme
T : Type v
inst✝¹ : TopologicalSpace T
inst✝ : TotallyDisconnectedSpace T
U : Scheme
f : C(ConnectedComponents ↥U, T)
⊢ ⇑f ∘ ConnectedComponents.mk = ⇑f ∘ ConnectedComponents.mk

Tactic:
simp

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₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ 𝟙 (F.obj ((data (F.obj X₀)).X i)) ≫ (data (F.obj X₀)).f i = (data (F.obj X₀)).f i

Tactic:
simp

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
i : (data X).I₀
⊢ ∀ (i_1 : (data (F.obj ((data X).X i))).I₀),
    presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) i_1 =
      (presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv) ≫
        presheafObjπ data G₀ (F.obj ((data X).X i)) i_1

Tactic:
intro j

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 : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j =
    (presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv) ≫
      presheafObjπ data G₀ (F.obj ((data X).X i)) j
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 : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ (data (F.obj ((data X).X i))).f j ≫ (data X).f i = (data (F.obj ((data X).X i))).f j ≫ (data X).f i

Tactic:
simp

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 : X₀ ⟶ Y₀
⊢ ∀ (i : (data (unop (op (F.obj X₀)))).I₀),
    (G₀.obj.map f.op ≫ (presheafObjObjIso data G₀ X₀).inv) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i =
      ((presheafObjObjIso data G₀ Y₀).inv ≫ presheafMap data G₀ (F.map f)) ≫
        presheafObjπ data G₀ (unop (op (F.obj X₀))) i

Tactic:
intro j

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₀ Y₀ : C₀
f : X₀ ⟶ Y₀
j : (data (unop (op (F.obj X₀)))).I₀
⊢ (G₀.obj.map f.op ≫ (presheafObjObjIso data G₀ X₀).inv) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) j =
    ((presheafObjObjIso data G₀ Y₀).inv ≫ presheafMap data G₀ (F.map f)) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) j
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Etale f → WeaklyEtale f

Tactic:
hf

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ WeaklyEtale f
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₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
⊢ (z ≫ kernel.ι b ≫ biprod.inr) ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.g =
    0

Tactic:
simp

Goal state after:
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
⊢ (ConcreteCategory.hom ((J.yoneda.map f).hom.app (op X))) (𝟙 X) = f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app (op X'))) f =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))

Tactic:
simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app (op X'))) f = (ConcreteCategory.hom (F.obj.map f.op)) x
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
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
inst✝ : IsFiltered J
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 : Mono f
⊢ ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk f

Tactic:
intro j

Goal state after:
case a
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
inst✝ : IsFiltered J
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 : Mono f
j : J
⊢ Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk 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
j₀ : J
y : X ⟶ Y.obj j₀
j : Under j₀
⊢ (kernel.ι (g y)).app j ≫ (constCocone (Under j₀) X).ι.app j = (kernel.ι (g y)).app j

Tactic:
simp

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

Goal state before:
pp: 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)
Y Z : C
g : Z ⟶ Y
u : (Sieve.ofArrows X c.inj).functor.obj (op Y)
⊢ (g ≫ Sieve.ofArrows.h ⋯) ≫ c.inj (Sieve.ofArrows.i ⋯) = Sieve.ofArrows.h ⋯ ≫ c.inj (Sieve.ofArrows.i ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
hi : IsMax (last n)
⊢ lastCases (last n) succ (last n) = last n

Tactic:
simp

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
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom

Tactic:
intro j

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 : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
j : J
⊢ Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: 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)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = CategoryTheory.yoneda.map (c.inj j)
Z : Cᵒᵖ
g : unop Z ⟶ X j
h : (Sieve.ofArrows X c.inj).arrows (g ≫ c.inj j)
⊢ Sieve.ofArrows.h h ≫ c.inj (Sieve.ofArrows.i h) = g ≫ c.inj j

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Bot α
⊢ (equivShrink α) ((equivShrink α).symm ⊥) = (equivShrink α) ⊥

Tactic:
simp

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

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ i = ⟨Order.succ ↑i, ⋯⟩

Tactic:
by
  ext
  simp only [coe_succ_of_not_isMax hi]

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ c.g₁ ≫ (Arrow.leftFunc.mapIso e).hom = (Iso.refl c.cofan₁.pt).hom ≫ c.g₁ ≫ Arrow.leftFunc.map e.hom

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ c.m ≫ (Iso.refl c.cofan₂.pt).hom = (Iso.refl c.cofan₁.pt).hom ≫ c.m

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
⊢ Arrow.mk ((h.iic j).F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
have eq : Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
      Arrow.mk (homOfLE (Order.le_succ i.1)) :=
        Arrow.ext rfl (Set.Iic.coe_succ_of_not_isMax hi) rfl

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (⋯.functor.map (homOfLE ⋯)) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk ((h.iic j).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ f ≫ (Arrow.rightFunc.mapIso e).hom = (Arrow.leftFunc.mapIso e).hom ≫ f'

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ c.g₂ ≫ (Arrow.rightFunc.mapIso e).hom = (Iso.refl c.cofan₂.pt).hom ≫ c.g₂ ≫ Arrow.rightFunc.map e.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X : C
⊢ ∀ (i : Fin 0), W ((ComposableArrows.mk₀ X).map (homOfLE ⋯))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
ι : Type w
X Y : C
F₁ F₂ : Discrete ι ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
φ : F₁ ⟶ F₂
hφ : (ofHoms g).functorCategory (Discrete ι) φ
g₁ : c₁.pt ⟶ X₁
g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i ↦ ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i ↦ eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i } ≅ A (π i) := fun i ↦ Arrow.leftFunc.mapIso (e i)
e₂ : (i : ι) → F₂.obj { as := i } ≅ B (π i) := fun i ↦ Arrow.rightFunc.mapIso (e i)
⊢ ∀ (j : Discrete ι),
    c₁.ι.app j ≫ (Iso.refl c₁.pt).hom =
      ((Cocone.precompose
                  (Discrete.natIso fun x ↦
                      match x with
                      | { as := i } => e₁ i).hom).obj
              (Cofan.mk c₁.pt fun i ↦ (e₁ i).inv ≫ c₁.ι.app { as := i })).ι.app
        j

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
ι : Type w
X Y : C
F₁ F₂ : Discrete ι ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
φ : F₁ ⟶ F₂
hφ : (ofHoms g).functorCategory (Discrete ι) φ
g₁ : c₁.pt ⟶ X₁
g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i ↦ ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i ↦ eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i } ≅ A (π i) := fun i ↦ Arrow.leftFunc.mapIso (e i)
e₂ : (i : ι) → F₂.obj { as := i } ≅ B (π i) := fun i ↦ Arrow.rightFunc.mapIso (e i)
⊢ ∀ (j : Discrete ι),
    c₂.ι.app j ≫ (Iso.refl c₂.pt).hom =
      ((Cocone.precompose
                  (Discrete.natIso fun x ↦
                      match x with
                      | { as := i } => e₂ i).hom).obj
              (Cofan.mk c₂.pt fun i ↦ (e₂ i).inv ≫ c₂.ι.app { as := i })).ι.app
        j

Tactic:
simp

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

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X : C
⊢ Φ.toSucc X = Φ.toSucc X ≫ eqToHom ⋯

Tactic:
simp

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
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
⊢ i ≤ i

Tactic:
simp

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

Goal state before:
pp: 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
A B : C
f : A ⟶ B
⊢ W.transfiniteCompositionsOfShape J f → transfiniteCompositions.{w, v, u} W f

Tactic:
hf

Goal state after:
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
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W f
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
⊢ transfiniteCompositions.{w, v, u} W₁ f → transfiniteCompositions.{w, v, u} W₂ f

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W₁ f
⊢ transfiniteCompositions.{w, v, u} W₂ f
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
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ k ≤ k

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ transfiniteCompositions.{w, v, u} W f → W f

Tactic:
hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W f
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
⊢ ¬j < j

Tactic:
simp

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 : J
hi : i ≤ j
⊢ map c i i ⋯ hi = 𝟙 (obj c i)

Tactic:
dsimp [map]
  grind

Goal state after:
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
⊢ j ∈ Set.Iic j

Tactic:
simp

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 : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
hj₂ : (iter₁.trunc h₀).F = (iter₂.trunc h₀).F
⊢ j ∈ Set.Iic j

Tactic:
simp

Goal state after:
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
⊢ Order.succ j ∈ Set.Iic (Order.succ j)

Tactic:
simp

Goal state after:
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
⊢ j ∈ Set.Iic j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
x : FunctorObjIndex f πX
⊢ A ((equivShrink I).symm ((equivShrink I) x.i)) = A x.i

Tactic:
simp

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 : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : k₁ ≤ j
⊢ j ≤ j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
x : FunctorObjIndex f πX
⊢ B ((equivShrink I).symm ((equivShrink I) x.i)) = B x.i

Tactic:
simp

Goal state after: