awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
rw :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯)) =
    Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ : arrowSucc iter.F i hi = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₃ rw₄ :
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) =
    Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ Φ.prop (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯))

Tactic:
rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]

Premises used: CategoryTheory.SmallObject.SuccStruct.prop_iff, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, CategoryTheory.SmallObject.SuccStruct.arrowMap, CategoryTheory.SmallObject.SuccStruct.arrowSucc_def
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
⊢ iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij) = colimit (restrictionLT iter.F hij)

Tactic:
congr_arg Comma.right (iter.arrowMap_limit i hi hij ⊥ (Order.IsSuccLimit.bot_lt hi))

Premises used: CategoryTheory.Comma.right, Bot.bot, CategoryTheory.Limits.colimit, congr_arg, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
refine :
  ∀ (j_1 : (↑(Set.Iio i) : Type w)),
    (colimit.cocone (restrictionLT iter.F hij)).ι.app j_1 ≫ Iso.hom (eqToIso ⋯) = (coconeOfLE iter.F hij).ι.app j_1
⊢ IsColimit (coconeOfLE iter.F hij)

Tactic:
refine IsColimit.ofIsoColimit (colimit.isColimit (restrictionLT iter.F hij))
    (Cocone.ext (eqToIso (iter.obj_limit i hi hij).symm) ?_)
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
a :
  Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      ((colimit.cocone (restrictionLT iter.F hij)).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫
        Iso.hom (eqToIso ⋯)) =
    Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      ((coconeOfLE iter.F hij).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
⊢ Eq (α :=
    (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶ (coconeOfLE iter.F hij).pt)
    ((colimit.cocone (restrictionLT iter.F hij)).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫
      Iso.hom (eqToIso ⋯))
    ((coconeOfLE iter.F hij).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))

Tactic:
apply Arrow.mk_injective

Premises used: CategoryTheory.Arrow.mk_injective
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
a :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯))
      (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom ⋯ :
        iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯) ⟶
          iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) =
    Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) (iter.F.map (homOfLE ⋯))
⊢ Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      ((colimit.cocone (restrictionLT iter.F hij)).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫
        Iso.hom (eqToIso ⋯)) =
    Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      ((coconeOfLE iter.F hij).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
a :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯))
      (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom ⋯ :
        iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯) ⟶
          iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) =
    arrowMap iter.F
      (↑(((Set.principalSegIioIicOfLE hij).toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s :=
                fun (x1 x2 : (↑(Set.Iic j) : Type w)) ↦ x1 < x2) :
              (a : (↑(Set.Iio i) : Type w)) → (↑(Set.Iic j) : Type w))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) :
        J)
      (↑((Set.principalSegIioIicOfLE hij).top (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s :=
            fun (x1 x2 : (↑(Set.Iic j) : Type w)) ↦ x1 < x2)) :
        J)
      ⋯ hij
⊢ Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯))
      (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom ⋯ :
        iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯) ⟶
          iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) =
    Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) (iter.F.map (homOfLE ⋯))

Tactic:
rw [← arrowMap]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMap
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯))
      (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom ⋯ :
        iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯) ⟶
          iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) =
    arrowMap iter.F
      (↑(((Set.principalSegIioIicOfLE hij).toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s :=
                fun (x1 x2 : (↑(Set.Iic j) : Type w)) ↦ x1 < x2) :
              (a : (↑(Set.Iio i) : Type w)) → (↑(Set.Iic j) : Type w))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) :
        J)
      (↑((Set.principalSegIioIicOfLE hij).top (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s :=
            fun (x1 x2 : (↑(Set.Iic j) : Type w)) ↦ x1 < x2)) :
        J)
      ⋯ hij

Tactic:
simp [iter.arrowMap_limit i hi hij k hk, arrowι_def]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowι_def, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯)

Tactic:
congr_arg Comma.left h

Premises used: CategoryTheory.Comma.left, congr_arg
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)

Tactic:
congr_arg Comma.right h

Premises used: CategoryTheory.Comma.right, congr_arg
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
K : Type w
inst_6 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
rw rw₁ :
  G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯)
⊢ F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯)

Tactic:
rw [h.src]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.src
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
K : Type w
inst_6 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
rw rw₁ :
  G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)
⊢ G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)

Tactic:
rw [h.tgt]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)),
    F.map (homOfLE h₁₂) = eqToHom hX ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯

Tactic:
have := (Arrow.mk_eq_mk_iff _ _).1 h
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
this :
  ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)),
    F.map (homOfLE h₁₂) = eqToHom hX ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
tauto tauto₁ tauto₂ :
  ∀
    (w :
      F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
        G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯))
    (w_1 :
      F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
        G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)),
    F.map (homOfLE h₁₂) = eqToHom w ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯ →
      F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
⊢ F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
K : Type w
inst_6 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k : K
hk : k ≤ x
h :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk)
⊢ k ≤ k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k : K
hk : k ≤ x
h :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk)
rw : arrowMap F k k ⋯ hk = arrowMap G k k ⋯ hk
rw₁ : Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))) = arrowMap G k k ⋯ hk
rw₂ :
  Eq (α := Arrow.{v, u} C) (Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
    (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
rw₃ rw₄ :
  Eq (α := Arrow.{v, u} C) (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
    (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
⊢ MapEq F G k k ⋯ hk

Tactic:
rw [MapEq, arrowMap_refl, arrowMap_refl, h]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMap_refl, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
simp :
  ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃)),
    F.map (homOfLE ⋯) = eqToHom hX ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯
⊢ MapEq F G i₁ i₃ ⋯ h₃

Tactic:
simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq, CategoryTheory.SmallObject.SuccStruct.arrowMap, CategoryTheory.Arrow.mk_eq_mk_iff
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃)),
    F.map (homOfLE ⋯) = eqToHom hX ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
⟨m₁₂.src, m₂₃.tgt, ?_⟩

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.src, Exists.intro
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
refine : F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯
⊢ ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃)),
    F.map (homOfLE ⋯) = eqToHom hX ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
rw : F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom ⋯
⊢ F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]

Premises used: CategoryTheory.homOfLE_comp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom ⋯

Tactic:
simp [-homOfLE_comp, m₁₂.w, m₂₃.w]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w, CategoryTheory.homOfLE_comp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
h₁ : ∀ ⦃X Y : (↑(Set.Iic x) : Type w)⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)
⊢ F = G

Tactic:
apply Arrow.functor_ext

Premises used: CategoryTheory.Arrow.functor_ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) 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 :
  Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ property ⟶
    Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂
⊢ F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter₁ iter₂ : Φ.Iteration j
this : iter₁.F = iter₂.F
⊢ iter₁ = iter₂

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter₁ iter₂ : Φ.Iteration j
suffices : iter₁.F = iter₂.F
⊢ iter₁ = iter₂

Tactic:
suffices iter₁.F = iter₂.F by aesop
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter₁ iter₂ : Φ.Iteration j
revert : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
⊢ iter₁.F = iter₂.F

Tactic:
revert iter₁ iter₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h : IsMin j
isMin : ∀ (h : IsMin.{w} (α := J) ⊥) (iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥), iter₁.F = iter₂.F
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F

Tactic:
obtain rfl := h.eq_bot

Premises used: IsMin.eq_bot, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
⊢ iter₁.F = iter₂.F

Tactic:
ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
isMin : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ ⊥), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
⊢ iter₁.F = iter₂.F

Tactic:
refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ ⊥
⊢ k₂ = ⊥

Tactic:
simpa using h₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ ⊥
isMin : ∀ (h₁₂ : k₁ ≤ ⊥) (h₂ : LE.le.{w} (α := J) ⊥ ⊥), MapEq iter₁.F iter₂.F k₁ ⊥ h₁₂ h₂
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
obtain rfl : k₂ = ⊥ := by simpa using h₂

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
k₁ : J
h₁₂ : k₁ ≤ ⊥
h₂ : LE.le.{w} (α := J) ⊥ ⊥
⊢ k₁ = ⊥

Tactic:
simpa using h₁₂