mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Shrink

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

Tactic:
obtain ⟨a, rfl⟩ := (equivShrink.{u} α).symm.surjective a
    obtain ⟨b, rfl⟩ := (equivShrink.{u} α).symm.surjective b
    simp only [Equiv.apply_symm_apply]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
X Y : C
f : X ⟶ Y
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : ↑(Set.Iic j)
φ : i ⟶ i'
⊢ c.F.map (⋯.functor.map φ ≫ homOfLE ⋯) = c.F.map (homOfLE ⋯)

Tactic:
rfl

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X✝ X Y : C
⊢ Arrow.mk (Φ.toSucc X✝) = Φ.toSuccArrow X✝

Tactic:
rfl

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
⊢ Φ.succ X = Φ.succ X

Tactic:
rfl

Goal state after:
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₂
⊢ ∀ ⦃X Y : ↑(Set.Iic x)⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)

Tactic:
rintro ⟨k₁, _⟩ ⟨k₂, h₂⟩ f

Goal state after:
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₂
k₁ : K
property✝ : k₁ ∈ Set.Iic x
k₂ : K
h₂ : k₂ ∈ Set.Iic x
f : ⟨k₁, property✝⟩ ⟶ ⟨k₂, h₂⟩
⊢ F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk 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
i₁ i₂ : J
hi : i₁ ≤ i₂
F : ↑(Set.Iio i₂) ⥤ C
c : Cocone F
hi₂ : i₂ ≤ i₂
h₂ : ¬i₂ < i₂
h₁ : i₁ < i₂
⊢ obj c i₂ = obj c i₂

Tactic:
rfl

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
i₂ : J
hi : i₂ ≤ i₂
F : ↑(Set.Iio i₂) ⥤ C
c : Cocone F
hi₂ : i₂ ≤ i₂
h₂ h₁ : ¬i₂ < i₂
⊢ obj c i₂ = obj c i₂

Tactic:
rfl

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

Tactic:
rfl

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
⊢ (if h₂ : i < j then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < j then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

Tactic:
grind

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

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

Tactic:
dif_pos hi₃',

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

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

Tactic:
dif_pos hi₃',

Goal state after:
case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    ((objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ ⋯).inv) ≫
      (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
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 ≤ Order.succ j

Tactic:
rfl

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:
rfl

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
i : J
hi : i ≤ Order.succ j
⊢ i ≤ i

Tactic:
rfl

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
⊢ Small.{t, max v w} (attachCellsιFunctorObj f πX).ι

Tactic:
by
  dsimp
  infer_instance

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
this : restrictionLE iter₁.F ⋯ = restrictionLE iter₂.F ⋯
⊢ ?m.491 ≤ k₂

Tactic:
rfl

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
k₁ k₂ : J
h : k₁ ≤ k₂
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ arrowMap (iter₂.trunc hj).F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
rfl

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
iter : Φ.Iteration j
k l : J
h : k ≤ l
h' : l ≤ j
⊢ j ≤ j

Tactic:
rfl

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

Goal state before:
pp: case e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ arrowMap iter.F ↑(⋯.functor.obj ⟨k₁, h₁⟩) ↑(⋯.functor.obj ⟨k₂, h₂⟩) ⋯ ⋯ =
    arrowMap iter.F ↑(⋯.functor.obj ⟨k₁, h₁⟩) ↑(⋯.functor.obj ⟨k₂, h₂⟩) ⋯ ?e_F.hi₂

pp: case e_F.hi₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ ↑(⋯.functor.obj ⟨k₂, h₂⟩) ≤ j

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯ ≫ f)

Tactic:
rfl

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 ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (⋯.functor.map f.unop).op))) val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val

Tactic:
rfl

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

Goal state before:
pp: case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val =
    (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val

Tactic:
rfl

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

Goal state before:
pp: case mk.mk
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val✝ : F.obj (op j)
map_zero✝¹ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = val₀
map_succ✝¹ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (ConcreteCategory.hom (F.map (homOfLE hij).op)) val✝ =
      d.lift i hi
        ⟨fun x ↦
          match x with
          | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝,
          ⋯⟩
map_zero✝ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
    val₀
map_succ✝ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
        { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
      d.succ i ⋯
        ((ConcreteCategory.hom (F.map (homOfLE ⋯).op))
          { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (ConcreteCategory.hom (F.map (homOfLE hij).op))
        { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
      d.lift i hi
        ⟨fun x ↦
          match x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
              { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val,
          ⋯⟩
⊢ { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ } =
    { val := { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val,
      map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }

Tactic:
rfl

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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
⊢ i ≤ i

Tactic:
rfl

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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
⊢ i ≤ i

Tactic:
rfl

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
j : J
e : d.Extension val₀ j
i : J
h : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE h).op)) e.val = (e.ofLE h).val

Tactic:
rfl

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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) (d.succ j hj e.val)

Tactic:
rfl

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
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)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ F.map (homOfLE ⋯) ≫ ⋯.lift = F.map (homOfLE ⋯ ≫ homOfLE ⋯) ≫ ⋯.lift

Tactic:
rfl

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

Goal state before:
pp: case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)

Tactic:
rfl

Goal state after:
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).retracts ≤ W.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]

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).retracts ≤ W.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp
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
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
⊢ i ≤ i

Tactic:
rfl

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 κ
f : Arrow C
⊢ Arrow.Hom.left (𝟙 ((iteration I κ).obj f)) = 𝟙 (obj I κ f.hom)

Tactic:
rfl

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 κ
f g h : Arrow C
φ : f ⟶ g
ψ : g ⟶ h
⊢ Arrow.Hom.left ((iteration I κ).map φ ≫ (iteration I κ).map ψ) =
    Arrow.Hom.left ((iteration I κ).map φ) ≫ Arrow.Hom.left ((iteration I κ).map ψ)

Tactic:
rfl

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp

Tactic:
exact antitone_rlp (generatingMonomorphisms_le_monomorphisms _)

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
inst✝ : IsGrothendieckAbelian.{w, v, u} C
X : C
⊢ Injective (monoMapFactorizationDataRlp 0).Z

Tactic:
let fac := (monoMapFactorizationDataRlp (0 : X ⟶ 0))
  simpa only [injective_iff_rlp_monomorphisms_zero,
    (isZero_zero C).eq_of_tgt fac.p 0] using fac.hp

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 κ
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
refine le_antisymm ?_
    (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp 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 κ
⊢ I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Tactic:
by simp [padicNorm, hq]

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

Goal state before:
pp: p : ℕ
q : ℚ
hq : ¬q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
by simp [padicNorm, hq]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)

Tactic:
←
        emultiplicity_le_emultiplicity_iff

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ ↑p ^ (-1) < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1

Tactic:
zpow_lt_zpow_iff_right₀ this

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑x = 0 ↔ x = 0

Tactic:
by rw [← coe_zero, Subtype.coe_inj]

Goal state after: