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

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
x✝ : J
h₁ : Order.IsSuccLimit x✝
h₂ : x✝ ≤ ⊥
⊢ x✝ = ⊥
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
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₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ arrowMap iter.F i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
← arrowSucc_def _ _ hi₁,

Goal state after:
case inl
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₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ arrowSucc iter.F i hi₁ = Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)
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
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
simpa using

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
i : J
hi : IsMin i
⊢ i = ⊥
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
ι : Type t
inst✝ : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : ι → ↑(ofHoms f).toSet := fun i ↦ ⟨Arrow.mk (f i), ⋯⟩
hφ : Function.Surjective φ
⊢ IsSmall.{w, v, u} (ofHoms f)

Tactic:
exact ⟨small_of_surjective hφ⟩

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 ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
simpa using

Goal state after:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ i = ⊥
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 ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
⊢ i = ⊥

Tactic:
simpa using

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
⊢ i = ⊥
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 ⊥)
hi : Order.IsSuccLimit ⊥
hij : ⊥ ≤ ⊥
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) val₀ =
    d.lift ⊥ hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀,
        ⋯⟩

Tactic:
simpa using

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
hi : Order.IsSuccLimit ⊥
hij : ⊥ ≤ ⊥
⊢ val₀ = d.lift ⊥ hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀, ⋯⟩
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
h : ⊥ < j
⊢ (↑s (Opposite.op ⟨⊥, h⟩)).f' = f

Tactic:
simpa using

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
⊢ (↑s (Opposite.op ⟨⊥, h⟩)).f' = f
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: case isMin
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
hj : IsMin ⊥
⊢ c.incl.app ⊥ ≫ φ₁ = c.incl.app ⊥ ≫ φ₂

Tactic:
simpa using

Goal state after:
case isMin
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
hj : IsMin ⊥
⊢ f ≫ φ₁ = f ≫ φ₂
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: case succ.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₁ = c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
simpa using

Goal state after:
case succ.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: case succ.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
i : (c.attachCells j hj).ι
⊢ (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
simpa using

Goal state after:
case succ.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
i : (c.attachCells j hj).ι
⊢ (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, c.incl.app b ≫ φ₁ = c.incl.app b ≫ φ₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₁ =
    ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₂

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, c.incl.app b ≫ φ₁ = c.incl.app b ≫ φ₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ c.incl.app k ≫ φ₁ = c.incl.app k ≫ φ₂
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
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
sq : CommSq f (c.ι.app ⊥) p g✝
s : ↑(sqFunctor c p f g✝).sections
hs : (↑s (Opposite.op ⊥)).f' = f
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ (↑s (Opposite.op j')).f' = (↑s (Opposite.op j)).f' ≫ ((Functor.const J).obj X).map g

Tactic:
simpa using

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
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
sq : CommSq f (c.ι.app ⊥) p g✝
s : ↑(sqFunctor c p f g✝).sections
hs : (↑s (Opposite.op ⊥)).f' = f
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ (↑s (Opposite.op j')).f' = (↑s (Opposite.op j)).f'
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ ⊥ < j

Tactic:
simpa using

Goal state after:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ ¬j = ⊥
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 ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ ↑⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩
      (op ⟨⊥, ⋯⟩) =
    val₀

Tactic:
simpa using

Goal state after:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ (e ⊥ ⋯).val = val₀
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

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
⊢ (coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
simpa using

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
⊢ (coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W ≤ W.rlp.llp
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 κ
j : κ.ord.ToType
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

Tactic:
have := hasIterationOfShape 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 κ
j : κ.ord.ToType
this : HasIterationOfShape κ.ord.ToType C
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))
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
⊢ RelativeCellComplex (fun x ↦ I.homFamily) (ιObj I κ f)

Tactic:
have := hasIterationOfShape 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
f : X ⟶ Y
this : HasIterationOfShape κ.ord.ToType C
⊢ RelativeCellComplex (fun x ↦ I.homFamily) (ιObj I κ f)
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
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ (ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) a = f

Tactic:
simpa using

Goal state after:
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
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ a ≫ p = f
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 A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ¬IsIso f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ¬Subobject.mk f = ⊤
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) =
    ↑(multiplicity (↑p) (c * q.num)) - ↑(multiplicity (↑p) (c * ↑q.den))

Tactic:
rw [multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1),
    multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1)]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) =
    ↑(multiplicity (↑p) c + multiplicity (↑p) q.num) - ↑(multiplicity (↑p) c + multiplicity ↑p ↑q.den)

p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ FiniteMultiplicity (↑p) (c * ↑q.den)

p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ FiniteMultiplicity (↑p) (c * q.num)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ FiniteMultiplicity (↑p) (c * ↑q.den)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ¬c = 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ FiniteMultiplicity (↑p) (c * q.num)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ¬c = 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ q * r = q.num * r.num /. (↑q.den * ↑r.den)

Tactic:
Rat.mul_eq_mkRat,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ mkRat (q.num * r.num) (q.den * r.den) = q.num * r.num /. (↑q.den * ↑r.den)
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
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)
h : Function.Injective fun j ↦ transfiniteIterate (largerSubobject hG) j A₀
⊢ False

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)
h : Function.Injective fun j ↦ transfiniteIterate (largerSubobject hG) j A₀
⊢ False
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this : Fact κ.IsRegular
⊢ Nonempty κ.ord.ToType

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this : Fact κ.IsRegular
⊢ ¬κ = 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : q = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : q = 0
⊢ 0 ≤ padicValRat p r
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
X : C
fac : (monomorphisms C).MapFactorizationData (monomorphisms C).rlp 0 := monoMapFactorizationDataRlp 0
⊢ Injective (monoMapFactorizationDataRlp 0).Z

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
X : C
fac : (monomorphisms C).MapFactorizationData (monomorphisms C).rlp 0 := monoMapFactorizationDataRlp 0
⊢ (monomorphisms C).rlp 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : q + r = 0
⊢ padicNorm p (q + r) ≤ padicNorm p q

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : q + r = 0
⊢ 0 ≤ padicNorm p q
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ i < n, 0 < padicValRat p (F i)
hn0 : ∑ i ∈ Finset.range n, F i ≠ 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range n, F i)

Tactic:
induction n with
  | zero => exact False.elim (hn0 rfl)
  | succ d hd =>
    rw [Finset.sum_range_succ] at hn0 ⊢
    by_cases h : ∑ x ∈ Finset.range d, F x = 0
    · rw [h, zero_add]
      exact hF d (lt_add_one _)
    · refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
      refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
      exact hF _ (lt_trans hi (lt_add_one _))

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpen {y | ‖y‖ ≤ 1}

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpen {y | ‖y‖ ≤ 1}
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a n : ℕ
⊢ padicValNat p (a ^ n) = n * padicValNat p a

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a n : ℕ
⊢ padicValRat p (↑a ^ n) = ↑n * padicValRat p ↑a
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
f : CauSeq ℤ_[p] norm
x✝ : ℝ
hε : x✝ > 0
⊢ ∃ i, ∀ j ≥ i, (fun a ↦ ‖a‖) ((fun n ↦ ↑(↑f n)) j - (fun n ↦ ↑(↑f n)) i) < x✝

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
f : CauSeq ℤ_[p] norm
x✝ : ℝ
hε : x✝ > 0
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → ↑(padicNormE (↑(↑f j) - ↑(↑f i))) < x✝
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ min ↑x.valuation ↑y.valuation ≤ ↑(x + y).valuation

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ (↑x).valuation ≤ (↑x + ↑y).valuation ∨ (↑y).valuation ≤ (↑x + ↑y).valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ¬IsUnit z ↔ ‖z‖ < 1

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ¬IsUnit z ↔ ‖z‖ < 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ x.valuation

Tactic:
simpa using

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ ↑p ^ x.valuation