mathlib-initiative/mathlib-tactics huggingface dataset:
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
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₃
⊢ ¬i₃ < i₃

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✝)
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
x : FunctorObjIndex f πX
⊢ (x.t ≫ Arrow.Hom.left τ) ≫ πY = f x.i ≫ x.b ≫ Arrow.Hom.right τ

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
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

pp: case isSuccLimit.inr
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
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
· have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
        simp at this
        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]

Goal state after:
case isSuccLimit.inr
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
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
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✝)
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
⊢ functorObjTop f πX ≫ Arrow.Hom.left τ = functorMapSrc f τ ≫ functorObjTop f πY

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
⊢ j ∈ Set.Iic 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
⊢ ¬↑⟨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
⊢ ¬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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ b ≫ Arrow.Hom.right (𝟙 (Arrow.mk πX)) = b

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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ t ≫ Arrow.Hom.left (𝟙 (Arrow.mk πX)) = t

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)
i : I
t : A i ⟶ X
b : B i ⟶ S
sq : CommSq t (f i) πX b
⊢ (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := ⋯ } ≫ ρFunctorObj f πX) ≫ πFunctorObj f πX = b

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
⊢ j ≤ j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
⊢ j ∈ Set.Iic j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i j : J
iter : Φ.Iteration j
hi : i ≤ j
⊢ i ≤ i

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
⊢ i ≤ i

Tactic:
simp

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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : ↑(Set.Iio j)
⊢ ↑i ∈ Set.Iic ↑i

Tactic:
simp

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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : ↑(Set.Iio j)
f : i₁ ⟶ i₂
⊢ ↑i₁ ≤ ↑i₁

Tactic:
simp

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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : ↑(Set.Iio j)
f : i₁ ⟶ i₂
⊢ ↑i₂ ≤ ↑i₂

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
⊢ i ≤ i

Tactic:
simp

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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ i₁ ≤ i₁

Tactic:
simp

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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ i₂ ≤ i₂

Tactic:
simp

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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
this : HasColimitsOfShape (↑(Set.Iio j)) C := hasColimitsOfShape_of_isSuccLimit C j hj
⊢ j ≤ j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
⊢ i ≤ i

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 ≤ j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
this : Arrow.mk ((Φ.iter (Order.succ j)).F.map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iter (Order.succ j)).F.obj ⟨j, ⋯⟩)
⊢ Order.succ j ≤ Order.succ j

Tactic:
simp

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

Goal state before:
pp: case h₁.h₀
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✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ pushout.inl (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) ≫
      pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
        (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ')) (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ =
    pushout.inl (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) ≫
      pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom)
          (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ ≫
        pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom)
          (functorObjLeft f π₃.hom) (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯

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✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ (b ≫ Arrow.Hom.right τ) ≫ Arrow.Hom.right τ' = b ≫ Arrow.Hom.right τ ≫ Arrow.Hom.right τ'

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✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ (t ≫ Arrow.Hom.left τ) ≫ Arrow.Hom.left τ' = t ≫ Arrow.Hom.left (τ ≫ τ')

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm ((equivShrink ↑W.toSet) ⟨Arrow.mk f, hf⟩))).hom

Tactic:
simp

Goal state after:
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 ⊥)
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀ = val₀

Tactic:
simp

Goal state after:
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
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
inst✝ : SuccOrder J
⊢ sq'.f' ≫ p = F.map (homOfLE ⋯) ≫ c.ι.app (Order.succ j) ≫ g

Tactic:
simp

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

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

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W.rlp.llp f
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
f : X ⟶ Y
⊢ (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts ≤ (coproducts.{w, v, u} I).pushouts

Tactic:
simp

Goal state after:
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
f : X ⟶ Y
j : κ.ord.ToType
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
have h₁ := (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.w

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
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))).right.hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app (Arrow.mk f))).right.hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pullback.fst p f ≫ (Iso.refl X).hom =
    (Subobject.underlyingIso (pullback.snd p f)).symm.hom ≫
      (Subobject.underlyingIso (pullback.snd p f)).hom ≫ pullback.fst p f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pullback.snd p f ≫ (Iso.refl (Opposite.unop (Opposite.op G))).hom =
    (Subobject.underlyingIso (pullback.snd p f)).symm.hom ≫ (Subobject.mk (pullback.snd p f)).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫ (Iso.refl (pushout (pullback.fst p f) (pullback.snd p f))).hom =
    (Iso.refl X).hom ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫ (Iso.refl (pushout (pullback.fst p f) (pullback.snd p f))).hom =
    (Iso.refl (Opposite.unop (Opposite.op G))).hom ≫ pushout.inr (pullback.fst p f) (pullback.snd p f)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫ pushout.desc p f ⋯ = p

Tactic:
simp

Goal state after:
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
f : X ⟶ Y
j : κ.ord.ToType
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
have h₁ := (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.w
  have h₂ := (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.naturality
    (homOfLE (Order.le_succ j))
  dsimp at h₁ h₂
  rw [comp_id] at h₂
  rw [← cancel_mono (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom,
    ← cancel_mono ((ιIteration I κ).app f).right, assoc, assoc, assoc, assoc, assoc,
    Iso.inv_hom_id_assoc, πObj_ιIteration_app_right,
    iterationFunctorObjObjRightIso_ιIteration_app_right,
    ← cancel_epi (relativeCellComplexιObjFObjSuccIso I κ f j).hom, Iso.hom_inv_id_assoc]
  dsimp [relativeCellComplexιObjFObjSuccIso,
    relativeCellComplexιObj, transfiniteCompositionOfShapeιIterationAppRight]
  simp only [reassoc_of% h₁, comp_id, comp_id, Arrow.w_mk_right, ← h₂,
    NatTrans.comp_app, Arrow.comp_right,
    iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫ pushout.desc p f ⋯ = f

Tactic:
simp

Goal state after:
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 A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f =
    (relativeCellComplexιObj I κ f).incl.app j ≫ πObj I κ f

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
⊢ 0 ≤ padicValRat p ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
⊢ ↑(padicValNat p n) = padicValRat p ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ multiplicity p p = 1

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ largerSubobject hG ⊤ = ⊤

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
this : IsIso (largerSubobject hG ⊤).arrow
⊢ (asIso ⊤.arrow).hom ≫ (Arrow.mk (𝟙 X)).hom =
    (Arrow.mk (⊤.ofLE (largerSubobject hG ⊤) ⋯)).hom ≫ (asIso (largerSubobject hG ⊤).arrow).hom

Tactic:
simp

Goal state after: